Theorem rankr1 3518

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1. Proposition 9.15(2) of [TakeutiZaring] p. 79.

Hypothesis

Ref	Expression
rankr1.1	|- A e. V

Assertion

Ref	Expression
rankr1	|- (B = (rank` A) <-> (-. A e. (R1` B) /\ A e. (R1` suc B)))

Proof of Theorem rankr1

Step	Hyp	Ref	Expression
1		rankon 3515	. . . . 5 |- (rank` A) e. On
2		eleq1 1149	. . . . 5 |- (B = (rank` A) -> (B e. On <-> (rank` A) e. On))
3	1, 2	mpbiri 169	. . . 4 |- (B = (rank` A) -> B e. On)
4		eloni 2209	. . . . 5 |- (B e. On -> Ord B)
5		ordzsl 2366	. . . . . 6 |- (Ord B <-> (B = (/) \/ E.x e. On B = suc x \/ Lim B))
6		noel 1711	. . . . . . . . 9 |- -. A e. (/)
7		fveq2 2832	. . . . . . . . . . 11 |- (B = (/) -> (R1` B) = (R1` (/)))
8		r10 3495	. . . . . . . . . . 11 |- (R1` (/)) = (/)
9	7, 8	syl6eq 1140	. . . . . . . . . 10 |- (B = (/) -> (R1` B) = (/))
10	9	eleq2d 1156	. . . . . . . . 9 |- (B = (/) -> (A e. (R1` B) <-> A e. (/)))
11	6, 10	mtbiri 539	. . . . . . . 8 |- (B = (/) -> -. A e. (R1` B))
12	11	a1d 14	. . . . . . 7 |- (B = (/) -> (B = (rank` A) -> -. A e. (R1` B)))
13		visset 1350	. . . . . . . . . . . . . . 15 |- x e. V
14	13	sucid 2304	. . . . . . . . . . . . . 14 |- x e. suc x
15		eleq2 1150	. . . . . . . . . . . . . 14 |- (B = suc x -> (x e. B <-> x e. suc x))
16	14, 15	mpbiri 169	. . . . . . . . . . . . 13 |- (B = suc x -> x e. B)
17	16	adantl 305	. . . . . . . . . . . 12 |- ((x e. On /\ B = suc x) -> x e. B)
18		ontri1 2232	. . . . . . . . . . . . . 14 |- ((B e. On /\ x e. On) -> (B (_ x <-> -. x e. B))
19	18	bicon2d 404	. . . . . . . . . . . . 13 |- ((B e. On /\ x e. On) -> (x e. B <-> -. B (_ x))
20		eleq1a 1158	. . . . . . . . . . . . . . 15 |- (suc x e. On -> (B = suc x -> B e. On))
21	20	imp 277	. . . . . . . . . . . . . 14 |- ((suc x e. On /\ B = suc x) -> B e. On)
22		suceloni 2314	. . . . . . . . . . . . . 14 |- (x e. On -> suc x e. On)
23	21, 22	sylan 343	. . . . . . . . . . . . 13 |- ((x e. On /\ B = suc x) -> B e. On)
24		pm3.26 256	. . . . . . . . . . . . 13 |- ((x e. On /\ B = suc x) -> x e. On)
25	19, 23, 24	sylanc 361	. . . . . . . . . . . 12 |- ((x e. On /\ B = suc x) -> (x e. B <-> -. B (_ x))
26	17, 25	mpbid 170	. . . . . . . . . . 11 |- ((x e. On /\ B = suc x) -> -. B (_ x)
27	26	adantr 306	. . . . . . . . . 10 |- (((x e. On /\ B = suc x) /\ B = (rank` A)) -> -. B (_ x)
28		rankr1.1	. . . . . . . . . . . . . . . . . . 19 |- A e. V
29	28	rankval 3512	. . . . . . . . . . . . . . . . . 18 |- (rank` A) = |^|{y e. On | A e. (R1` suc y)}
30	29	cleq2i 1111	. . . . . . . . . . . . . . . . 17 |- (B = (rank` A) <-> B = |^|{y e. On | A e. (R1` suc y)})
31	30	biimp 133	. . . . . . . . . . . . . . . 16 |- (B = (rank` A) -> B = |^|{y e. On | A e. (R1` suc y)})
32	31	sseq1d 1527	. . . . . . . . . . . . . . 15 |- (B = (rank` A) -> (B (_ x <-> |^|{y e. On | A e. (R1` suc y)} (_ x))
33		suceq 2288	. . . . . . . . . . . . . . . . . . 19 |- (y = x -> suc y = suc x)
34	33	fveq2d 2836	. . . . . . . . . . . . . . . . . 18 |- (y = x -> (R1` suc y) = (R1` suc x))
35	34	eleq2d 1156	. . . . . . . . . . . . . . . . 17 |- (y = x -> (A e. (R1` suc y) <-> A e. (R1` suc x)))
36	35	onintss 2266	. . . . . . . . . . . . . . . 16 |- (x e. On -> (A e. (R1` suc x) -> |^|{y e. On | A e. (R1` suc y)} (_ x))
37	36	imp 277	. . . . . . . . . . . . . . 15 |- ((x e. On /\ A e. (R1` suc x)) -> |^|{y e. On | A e. (R1` suc y)} (_ x)
38	32, 37	syl5bir 184	. . . . . . . . . . . . . 14 |- (B = (rank` A) -> ((x e. On /\ A e. (R1` suc x)) -> B (_ x))
39		fveq2 2832	. . . . . . . . . . . . . . . 16 |- (B = suc x -> (R1` B) = (R1` suc x))
40	39	eleq2d 1156	. . . . . . . . . . . . . . 15 |- (B = suc x -> (A e. (R1` B) <-> A e. (R1` suc x)))
41	40	biimpa 324	. . . . . . . . . . . . . 14 |- ((B = suc x /\ A e. (R1` B)) -> A e. (R1` suc x))
42	38, 41	sylan2i 357	. . . . . . . . . . . . 13 |- (B = (rank` A) -> ((x e. On /\ (B = suc x /\ A e. (R1` B))) -> B (_ x))
43	42	exp4d 298	. . . . . . . . . . . 12 |- (B = (rank` A) -> (x e. On -> (B = suc x -> (A e. (R1` B) -> B (_ x))))
44	43	com3l 34	. . . . . . . . . . 11 |- (x e. On -> (B = suc x -> (B = (rank` A) -> (A e. (R1` B) -> B (_ x))))
45	44	imp31 280	. . . . . . . . . 10 |- (((x e. On /\ B = suc x) /\ B = (rank` A)) -> (A e. (R1` B) -> B (_ x))
46	27, 45	mtod 95	. . . . . . . . 9 |- (((x e. On /\ B = suc x) /\ B = (rank` A)) -> -. A e. (R1` B))
47	46	exp31 293	. . . . . . . 8 |- (x e. On -> (B = suc x -> (B = (rank` A) -> -. A e. (R1` B))))
48	47	r19.23aiv 1284	. . . . . . 7 |- (E.x e. On B = suc x -> (B = (rank` A) -> -. A e. (R1` B)))
49		eleq2 1150	. . . . . . . . . . . . . . . . . . 19 |- (B = (rank` A) -> (x e. B <-> x e. (rank` A)))
50	1	onel 2346	. . . . . . . . . . . . . . . . . . 19 |- (x e. (rank` A) -> x e. On)
51	49, 50	syl6bi 187	. . . . . . . . . . . . . . . . . 18 |- (B = (rank` A) -> (x e. B -> x e. On))
52	51	anc2li 250	. . . . . . . . . . . . . . . . 17 |- (B = (rank` A) -> (x e. B -> (B = (rank` A) /\ x e. On)))
53		r1ord2 3500	. . . . . . . . . . . . . . . . . . . . . . 23 |- (suc x e. On -> (x e. suc x -> (R1` x) (_ (R1` suc x)))
54	14, 53	mpi 44	. . . . . . . . . . . . . . . . . . . . . 22 |- (suc x e. On -> (R1` x) (_ (R1` suc x))
55	22, 54	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (x e. On -> (R1` x) (_ (R1` suc x))
56	55	sseld 1506	. . . . . . . . . . . . . . . . . . . 20 |- (x e. On -> (A e. (R1` x) -> A e. (R1` suc x)))
57	29	sseq1i 1524	. . . . . . . . . . . . . . . . . . . . 21 |- ((rank` A) (_ x <-> |^|{y e. On | A e. (R1` suc y)} (_ x)
58	36, 57	syl6ibr 186	. . . . . . . . . . . . . . . . . . . 20 |- (x e. On -> (A e. (R1` suc x) -> (rank` A) (_ x))
59	56, 58	syld 27	. . . . . . . . . . . . . . . . . . 19 |- (x e. On -> (A e. (R1` x) -> (rank` A) (_ x))
60		sseq1 1521	. . . . . . . . . . . . . . . . . . . 20 |- (B = (rank` A) -> (B (_ x <-> (rank` A) (_ x))
61	60	biimprd 136	. . . . . . . . . . . . . . . . . . 19 |- (B = (rank` A) -> ((rank` A) (_ x -> B (_ x))
62	59, 61	sylan9r 360	. . . . . . . . . . . . . . . . . 18 |- ((B = (rank` A) /\ x e. On) -> (A e. (R1` x) -> B (_ x))
63	18, 3	sylan 343	. . . . . . . . . . . . . . . . . 18 |- ((B = (rank` A) /\ x e. On) -> (B (_ x <-> -. x e. B))
64	62, 63	sylibd 177	. . . . . . . . . . . . . . . . 17 |- ((B = (rank` A) /\ x e. On) -> (A e. (R1` x) -> -. x e. B))
65	52, 64	syl6 23	. . . . . . . . . . . . . . . 16 |- (B = (rank` A) -> (x e. B -> (A e. (R1` x) -> -. x e. B)))
66	65	com3l 34	. . . . . . . . . . . . . . 15 |- (x e. B -> (A e. (R1` x) -> (B = (rank` A) -> -. x e. B)))
67		con2 82	. . . . . . . . . . . . . . 15 |- ((B = (rank` A) -> -. x e. B) -> (x e. B -> -. B = (rank` A)))
68	66, 67	syl6 23	. . . . . . . . . . . . . 14 |- (x e. B -> (A e. (R1` x) -> (x e. B -> -. B = (rank` A))))
69	68	pm2.43a 60	. . . . . . . . . . . . 13 |- (x e. B -> (A e. (R1` x) -> -. B = (rank` A)))
70	69	r19.23aiv 1284	. . . . . . . . . . . 12 |- (E.x e. B A e. (R1` x) -> -. B = (rank` A))
71	70	con2i 89	. . . . . . . . . . 11 |- (B = (rank` A) -> -. E.x e. B A e. (R1` x))
72	71	adantr 306	. . . . . . . . . 10 |- ((B = (rank` A) /\ Lim B) -> -. E.x e. B A e. (R1` x))
73		r1lim 3497	. . . . . . . . . . . . 13 |- ((B e. V /\ Lim B) -> (R1` B) = U.x e. B (R1` x))
74		fvex 2838	. . . . . . . . . . . . . 14 |- (rank` A) e. V
75		eleq1 1149	. . . . . . . . . . . . . 14 |- (B = (rank` A) -> (B e. V <-> (rank` A) e. V))
76	74, 75	mpbiri 169	. . . . . . . . . . . . 13 |- (B = (rank` A) -> B e. V)
77	73, 76	sylan 343	. . . . . . . . . . . 12 |- ((B = (rank` A) /\ Lim B) -> (R1` B) = U.x e. B (R1` x))
78	77	eleq2d 1156	. . . . . . . . . . 11 |- ((B = (rank` A) /\ Lim B) -> (A e. (R1` B) <-> A e. U.x e. B (R1` x)))
79		eliun 1998	. . . . . . . . . . 11 |- (A e. U.x e. B (R1` x) <-> E.x e. B A e. (R1` x))
80	78, 79	syl6bb 414	. . . . . . . . . 10 |- ((B = (rank` A) /\ Lim B) -> (A e. (R1` B) <-> E.x e. B A e. (R1` x)))
81	72, 80	mtbird 537	. . . . . . . . 9 |- ((B = (rank` A) /\ Lim B) -> -. A e. (R1` B))
82	81	exp 291	. . . . . . . 8 |- (B = (rank` A) -> (Lim B -> -. A e. (R1` B)))
83	82	com12 13	. . . . . . 7 |- (Lim B -> (B = (rank` A) -> -. A e. (R1` B)))
84	12, 48, 83	3jaoi 633	. . . . . 6 |- ((B = (/)