Theorem rankr1 4654

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 4651	. . . . 5 |- (rank` A) e. On
2		eleq1 1531	. . . . 5 |- (B = (rank` A) -> (B e. On <-> (rank` A) e. On))
3	1, 2	mpbiri 194	. . . 4 |- (B = (rank` A) -> B e. On)
4		eloni 2953	. . . . 5 |- (B e. On -> Ord B)
5		ordzsl 3111	. . . . . 6 |- (Ord B <-> (B = (/) \/ E.x e. On B = suc x \/ Lim B))
6		noel 2280	. . . . . . . . 9 |- -. A e. (/)
7		fveq2 3715	. . . . . . . . . . 11 |- (B = (/) -> (R1` B) = (R1` (/)))
8		r10 4631	. . . . . . . . . . 11 |- (R1` (/)) = (/)
9	7, 8	syl6eq 1520	. . . . . . . . . 10 |- (B = (/) -> (R1` B) = (/))
10	9	eleq2d 1538	. . . . . . . . 9 |- (B = (/) -> (A e. (R1` B) <-> A e. (/)))
11	6, 10	mtbiri 716	. . . . . . . 8 |- (B = (/) -> -. A e. (R1` B))
12	11	a1d 12	. . . . . . 7 |- (B = (/) -> (B = (rank` A) -> -. A e. (R1` B)))
13		visset 1809	. . . . . . . . . . . . . . 15 |- x e. V
14	13	sucid 3046	. . . . . . . . . . . . . 14 |- x e. suc x
15		eleq2 1532	. . . . . . . . . . . . . 14 |- (B = suc x -> (x e. B <-> x e. suc x))
16	14, 15	mpbiri 194	. . . . . . . . . . . . 13 |- (B = suc x -> x e. B)
17	16	adantl 388	. . . . . . . . . . . 12 |- ((x e. On /\ B = suc x) -> x e. B)
18		ontri1 2976	. . . . . . . . . . . . . 14 |- ((B e. On /\ x e. On) -> (B (_ x <-> -. x e. B))
19	18	con2bid 525	. . . . . . . . . . . . 13 |- ((B e. On /\ x e. On) -> (x e. B <-> -. B (_ x))
20		eleq1a 1540	. . . . . . . . . . . . . . 15 |- (suc x e. On -> (B = suc x -> B e. On))
21	20	imp 350	. . . . . . . . . . . . . 14 |- ((suc x e. On /\ B = suc x) -> B e. On)
22		suceloni 3057	. . . . . . . . . . . . . 14 |- (x e. On -> suc x e. On)
23	21, 22	sylan 448	. . . . . . . . . . . . 13 |- ((x e. On /\ B = suc x) -> B e. On)
24		pm3.26 319	. . . . . . . . . . . . 13 |- ((x e. On /\ B = suc x) -> x e. On)
25	19, 23, 24	sylanc 471	. . . . . . . . . . . 12 |- ((x e. On /\ B = suc x) -> (x e. B <-> -. B (_ x))
26	17, 25	mpbid 195	. . . . . . . . . . 11 |- ((x e. On /\ B = suc x) -> -. B (_ x)
27	26	adantr 389	. . . . . . . . . 10 |- (((x e. On /\ B = suc x) /\ B = (rank` A)) -> -. B (_ x)
28		rankr1.1	. . . . . . . . . . . . . . . . . . 19 |- A e. V
29	28	rankval 4648	. . . . . . . . . . . . . . . . . 18 |- (rank` A) = |^|{y e. On | A e. (R1` suc y)}
30	29	eqeq2i 1482	. . . . . . . . . . . . . . . . 17 |- (B = (rank` A) <-> B = |^|{y e. On | A e. (R1` suc y)})
31	30	biimp 151	. . . . . . . . . . . . . . . 16 |- (B = (rank` A) -> B = |^|{y e. On | A e. (R1` suc y)})
32	31	sseq1d 2084	. . . . . . . . . . . . . . 15 |- (B = (rank` A) -> (B (_ x <-> |^|{y e. On | A e. (R1` suc y)} (_ x))
33		suceq 3029	. . . . . . . . . . . . . . . . . . 19 |- (y = x -> suc y = suc x)
34	33	fveq2d 3719	. . . . . . . . . . . . . . . . . 18 |- (y = x -> (R1` suc y) = (R1` suc x))
35	34	eleq2d 1538	. . . . . . . . . . . . . . . . 17 |- (y = x -> (A e. (R1` suc y) <-> A e. (R1` suc x)))
36	35	onintss 3006	. . . . . . . . . . . . . . . 16 |- (x e. On -> (A e. (R1` suc x) -> |^|{y e. On | A e. (R1` suc y)} (_ x))
37	36	imp 350	. . . . . . . . . . . . . . 15 |- ((x e. On /\ A e. (R1` suc x)) -> |^|{y e. On | A e. (R1` suc y)} (_ x)
38	32, 37	syl5bir 210	. . . . . . . . . . . . . 14 |- (B = (rank` A) -> ((x e. On /\ A e. (R1` suc x)) -> B (_ x))
39		fveq2 3715	. . . . . . . . . . . . . . . 16 |- (B = suc x -> (R1` B) = (R1` suc x))
40	39	eleq2d 1538	. . . . . . . . . . . . . . 15 |- (B = suc x -> (A e. (R1` B) <-> A e. (R1` suc x)))
41	40	biimpa 416	. . . . . . . . . . . . . 14 |- ((B = suc x /\ A e. (R1` B)) -> A e. (R1` suc x))
42	38, 41	sylan2i 465	. . . . . . . . . . . . 13 |- (B = (rank` A) -> ((x e. On /\ (B = suc x /\ A e. (R1` B))) -> B (_ x))
43	42	exp4d 381	. . . . . . . . . . . 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 362	. . . . . . . . . 10 |- (((x e. On /\ B = suc x) /\ B = (rank` A)) -> (A e. (R1` B) -> B (_ x))
46	27, 45	mtod 108	. . . . . . . . 9 |- (((x e. On /\ B = suc x) /\ B = (rank` A)) -> -. A e. (R1` B))
47	46	exp31 376	. . . . . . . 8 |- (x e. On -> (B = suc x -> (B = (rank` A) -> -. A e. (R1` B))))
48	47	r19.23aiv 1740	. . . . . . 7 |- (E.x e. On B = suc x -> (B = (rank` A) -> -. A e. (R1` B)))
49		eleq2 1532	. . . . . . . . . . . . . . . . . 18 |- (B = (rank` A) -> (x e. B <-> x e. (rank` A)))
50	1	onel 3093	. . . . . . . . . . . . . . . . . 18 |- (x e. (rank` A) -> x e. On)
51	49, 50	syl6bi 214	. . . . . . . . . . . . . . . . 17 |- (B = (rank` A) -> (x e. B -> x e. On))
52	51	anc2li 302	. . . . . . . . . . . . . . . 16 |- (B = (rank` A) -> (x e. B -> (B = (rank` A) /\ x e. On)))
53		r1ord2 4636	. . . . . . . . . . . . . . . . . . . . . 22 |- (suc x e. On -> (x e. suc x -> (R1` x) (_ (R1` suc x)))
54	14, 53	mpi 44	. . . . . . . . . . . . . . . . . . . . 21 |- (suc x e. On -> (R1` x) (_ (R1` suc x))
55	22, 54	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (x e. On -> (R1` x) (_ (R1` suc x))
56	55	sseld 2063	. . . . . . . . . . . . . . . . . . 19 |- (x e. On -> (A e. (R1` x) -> A e. (R1` suc x)))
57	29	sseq1i 2081	. . . . . . . . . . . . . . . . . . . 20 |- ((rank` A) (_ x <-> |^|{y e. On | A e. (R1` suc y)} (_ x)
58	36, 57	syl6ibr 213	. . . . . . . . . . . . . . . . . . 19 |- (x e. On -> (A e. (R1` suc x) -> (rank` A) (_ x))
59	56, 58	syld 27	. . . . . . . . . . . . . . . . . 18 |- (x e. On -> (A e. (R1` x) -> (rank` A) (_ x))
60		sseq1 2078	. . . . . . . . . . . . . . . . . . 19 |- (B = (rank` A) -> (B (_ x <-> (rank` A) (_ x))
61	60	biimprd 154	. . . . . . . . . . . . . . . . . 18 |- (B = (rank` A) -> ((rank` A) (_ x -> B (_ x))
62	59, 61	sylan9r 469	. . . . . . . . . . . . . . . . 17 |- ((B = (rank` A) /\ x e. On) -> (A e. (R1` x) -> B (_ x))
63	18, 3	sylan 448	. . . . . . . . . . . . . . . . 17 |- ((B = (rank` A) /\ x e. On) -> (B (_ x <-> -. x e. B))
64	62, 63	sylibd 202	. . . . . . . . . . . . . . . 16 |- ((B = (rank` A) /\ x e. On) -> (A e. (R1` x) -> -. x e. B))
65	52, 64	syl6 22	. . . . . . . . . . . . . . 15 |- (B = (rank` A) -> (x e. B -> (A e. (R1` x) -> -. x e. B)))
66	65	com3l 34	. . . . . . . . . . . . . 14 |- (x e. B -> (A e. (R1` x) -> (B = (rank` A) -> -. x e. B)))
67		con2 90	. . . . . . . . . . . . . 14 |- ((B = (rank` A) -> -. x e. B) -> (x e. B -> -. B = (rank` A)))
68	66, 67	syl6 22	. . . . . . . . . . . . 13 |- (x e. B -> (A e. (R1` x) -> (x e. B -> -. B = (rank` A))))
69	68	pm2.43a 66	. . . . . . . . . . . 12 |- (x e. B -> (A e. (R1` x) -> -. B = (rank` A)))
70	69	r19.23aiv 1740	. . . . . . . . . . 11 |- (E.x e. B A e. (R1` x) -> -. B = (rank` A))
71	70	con2i 97	. . . . . . . . . 10 |- (B = (rank` A) -> -. E.x e. B A e. (R1` x))
72	71	adantr 389	. . . . . . . . 9 |- ((B = (rank` A) /\ Lim B) -> -. E.x e. B A e. (R1` x))
73		r1lim 4633	. . . . . . . . . . . 12 |- ((B e. V /\ Lim B) -> (R1` B) = U_x e. B (R1` x))
74		fvex 3723	. . . . . . . . . . . . 13 |- (rank` A) e. V
75		eleq1 1531	. . . . . . . . . . . . 13 |- (B = (rank` A) -> (B e. V <-> (rank` A) e. V))
76	74, 75	mpbiri 194	. . . . . . . . . . . 12 |- (B = (rank` A) -> B e. V)
77	73, 76	sylan 448	. . . . . . . . . . 11 |- ((B = (rank` A) /\ Lim B) -> (R1` B) = U_x e. B (R1` x))
78	77	eleq2d 1538	. . . . . . . . . 10 |- ((B = (rank` A) /\ Lim B) -> (A e. (R1` B) <-> A e. U_x e. B (R1` x)))
79		eliun 2565	. . . . . . . . . 10 |- (A e. U_x e. B (R1` x) <-> E.x e. B A e. (R1` x))
80	78, 79	syl6bb 535	. . . . . . . . 9 |- ((B = (rank` A) /\ Lim B) -> (A e. (R1` B) <-> E.x e. B A e. (R1` x)))
81	72, 80	mtbird 714	. . . . . . . 8