Theorem r1ord 4638

Description: Ordering relation for the cumulative hierarchy of sets. Part of Proposition 9.10(2) of [TakeutiZaring] p. 77.

Assertion

Ref	Expression
r1ord	|- (B e. On -> (A e. B -> (R1` A) e. (R1` B)))

Proof of Theorem r1ord

Step	Hyp	Ref	Expression
1		eleq2 1533	. . . . . 6 |- (x = suc A -> (A e. x <-> A e. suc A))
2		fveq2 3719	. . . . . . 7 |- (x = suc A -> (R1` x) = (R1` suc A))
3	2	eleq2d 1539	. . . . . 6 |- (x = suc A -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` suc A)))
4	1, 3	imbi12d 625	. . . . 5 |- (x = suc A -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. suc A -> (R1` A) e. (R1` suc A))))
5		eleq2 1533	. . . . . 6 |- (x = y -> (A e. x <-> A e. y))
6		fveq2 3719	. . . . . . 7 |- (x = y -> (R1` x) = (R1` y))
7	6	eleq2d 1539	. . . . . 6 |- (x = y -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` y)))
8	5, 7	imbi12d 625	. . . . 5 |- (x = y -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. y -> (R1` A) e. (R1` y))))
9		eleq2 1533	. . . . . 6 |- (x = suc y -> (A e. x <-> A e. suc y))
10		fveq2 3719	. . . . . . 7 |- (x = suc y -> (R1` x) = (R1` suc y))
11	10	eleq2d 1539	. . . . . 6 |- (x = suc y -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` suc y)))
12	9, 11	imbi12d 625	. . . . 5 |- (x = suc y -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. suc y -> (R1` A) e. (R1` suc y))))
13		eleq2 1533	. . . . . 6 |- (x = B -> (A e. x <-> A e. B))
14		fveq2 3719	. . . . . . 7 |- (x = B -> (R1` x) = (R1` B))
15	14	eleq2d 1539	. . . . . 6 |- (x = B -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` B)))
16	13, 15	imbi12d 625	. . . . 5 |- (x = B -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. B -> (R1` A) e. (R1` B))))
17		onelon 2968	. . . . . . 7 |- ((suc A e. On /\ A e. suc A) -> A e. On)
18		r1suc 4635	. . . . . . . 8 |- (A e. On -> (R1` suc A) = P~(R1` A))
19		fvex 3727	. . . . . . . . 9 |- (R1` A) e. V
20	19	pwid 2405	. . . . . . . 8 |- (R1` A) e. P~(R1` A)
21	18, 20	syl5eleqr 1553	. . . . . . 7 |- (A e. On -> (R1` A) e. (R1` suc A))
22	17, 21	syl 10	. . . . . 6 |- ((suc A e. On /\ A e. suc A) -> (R1` A) e. (R1` suc A))
23	22	ex 373	. . . . 5 |- (suc A e. On -> (A e. suc A -> (R1` A) e. (R1` suc A)))
24		r1suc 4635	. . . . . . . . . . . . . 14 |- (y e. On -> (R1` suc y) = P~(R1` y))
25		fvex 3727	. . . . . . . . . . . . . . 15 |- (R1` y) e. V
26	25	pwid 2405	. . . . . . . . . . . . . 14 |- (R1` y) e. P~(R1` y)
27	24, 26	syl5eleqr 1553	. . . . . . . . . . . . 13 |- (y e. On -> (R1` y) e. (R1` suc y))
28		r1tr 4637	. . . . . . . . . . . . . 14 |- Tr (R1` suc y)
29		trss 2685	. . . . . . . . . . . . . 14 |- (Tr (R1` suc y) -> ((R1` y) e. (R1` suc y) -> (R1` y) (_ (R1` suc y)))
30	28, 29	ax-mp 7	. . . . . . . . . . . . 13 |- ((R1` y) e. (R1` suc y) -> (R1` y) (_ (R1` suc y))
31	27, 30	syl 10	. . . . . . . . . . . 12 |- (y e. On -> (R1` y) (_ (R1` suc y))
32	31	sseld 2064	. . . . . . . . . . 11 |- (y e. On -> ((R1` A) e. (R1` y) -> (R1` A) e. (R1` suc y)))
33	32	imim2d 25	. . . . . . . . . 10 |- (y e. On -> ((A e. y -> (R1` A) e. (R1` y)) -> (A e. y -> (R1` A) e. (R1` suc y))))
34		elisset 1814	. . . . . . . . . . . . 13 |- (suc A e. On -> suc A e. V)
35		sucexb 3044	. . . . . . . . . . . . 13 |- (A e. V <-> suc A e. V)
36	34, 35	sylibr 200	. . . . . . . . . . . 12 |- (suc A e. On -> A e. V)
37		sucssel 3066	. . . . . . . . . . . 12 |- (A e. V -> (suc A (_ y -> A e. y))
38	36, 37	syl 10	. . . . . . . . . . 11 |- (suc A e. On -> (suc A (_ y -> A e. y))
39	38	imp 350	. . . . . . . . . 10 |- ((suc A e. On /\ suc A (_ y) -> A e. y)
40	33, 39	syl7 23	. . . . . . . . 9 |- (y e. On -> ((A e. y -> (R1` A) e. (R1` y)) -> ((suc A e. On /\ suc A (_ y) -> (R1` A) e. (R1` suc y))))
41	40	a1d 12	. . . . . . . 8 |- (y e. On -> (A e. suc y -> ((A e. y -> (R1` A) e. (R1` y)) -> ((suc A e. On /\ suc A (_ y) -> (R1` A) e. (R1` suc y)))))
42	41	com24 37	. . . . . . 7 |- (y e. On -> ((suc A e. On /\ suc A (_ y) -> ((A e. y -> (R1` A) e. (R1` y)) -> (A e. suc y -> (R1` A) e. (R1` suc y)))))
43	42	exp3a 375	. . . . . 6 |- (y e. On -> (suc A e. On -> (suc A (_ y -> ((A e. y -> (R1` A) e. (R1` y)) -> (A e. suc y -> (R1` A) e. (R1` suc y))))))
44	43	imp31 362	. . . . 5 |- (((y e. On /\ suc A e. On) /\ suc A (_ y) -> ((A e. y -> (R1` A) e. (R1` y)) -> (A e. suc y -> (R1` A) e. (R1` suc y))))
45		fveq2 3719	. . . . . . . . . . . . 13 |- (y = suc A -> (R1` y) = (R1` suc A))
46	45	eleq2d 1539	. . . . . . . . . . . 12 |- (y = suc A -> ((R1` A) e. (R1` y) <-> (R1` A) e. (R1` suc A)))
47	46	rcla4ev 1874	. . . . . . . . . . 11 |- ((suc A e. x /\ (R1` A) e. (R1` suc A)) -> E.y e. x (R1` A) e. (R1` y))
48		limsuc 3116	. . . . . . . . . . . 12 |- (Lim x -> (A e. x <-> suc A e. x))
49	48	biimpa 416	. . . . . . . . . . 11 |- ((Lim x /\ A e. x) -> suc A e. x)
50		onelon 2968	. . . . . . . . . . . . 13 |- ((x e. On /\ A e. x) -> A e. On)
51		limord 3024	. . . . . . . . . . . . . 14 |- (Lim x -> Ord x)
52		visset 1810	. . . . . . . . . . . . . . 15 |- x e. V
53	52	elon 2953	. . . . . . . . . . . . . 14 |- (x e. On <-> Ord x)
54	51, 53	sylibr 200	. . . . . . . . . . . . 13 |- (Lim x -> x e. On)
55	50, 54	sylan 448	. . . . . . . . . . . 12 |- ((Lim x /\ A e. x) -> A e. On)
56	55, 21	syl 10	. . . . . . . . . . 11 |- ((Lim x /\ A e. x) -> (R1` A) e. (R1` suc A))
57	47, 49, 56	sylanc 471	. . . . . . . . . 10 |- ((Lim x /\ A e. x) -> E.y e. x (R1` A) e. (R1` y))
58		eliun 2566	. . . . . . . . . 10 |- ((R1` A) e. U_y e. x (R1` y) <-> E.y e. x (R1` A) e. (R1` y))
59	57, 58	sylibr 200	. . . . . . . . 9 |- ((Lim x /\ A e. x) -> (R1` A) e. U_y e. x (R1` y))
60		r1lim 4636	. . . . . . . . . . . 12 |- ((x e. V /\ Lim x) -> (R1` x) = U_y e. x (R1` y))
61	52, 60	mpan 694	. . . . . . . . . . 11 |- (Lim x -> (R1` x) = U_y e. x (R1` y))
62	61	eleq2d 1539	. . . . . . . . . 10 |- (Lim x -> ((R1` A) e. (R1` x) <-> (R1` A) e. U_y e. x (R1` y)))
63	62	adantr 389	. . . . . . . . 9 |- ((Lim x /\ A e. x) -> ((R1` A) e. (R1` x) <-> (R1` A) e. U_y e. x (R1` y)))
64	59, 63	mpbird 196	. . . . . . . 8 |- ((Lim x /\ A e. x) -> (R1` A) e. (R1` x))
65	64	ex 373	. . . . . . 7 |- (Lim x -> (A e. x -> (R1` A) e. (R1` x)))
66	65	ad2antrr 404	. . . . . 6 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (A e. x -> (R1` A) e. (R1` x)))
67	66	a1d 12	. . . . 5 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (A.y e. x (suc A (_ y -> (A e. y -> (R1` A) e. (R1` y))) -> (A e. x -> (R1` A) e. (R1` x))))
68	4, 8, 12, 16, 23, 44, 67	tfindsg 3158	. . . 4 |- (((B e. On /\ suc A e. On) /\ suc A (_ B) -> (A e. B -> (R1` A) e. (R1` B)))
69		pm3.26 319	. . . . 5 |- ((B e. On /\ A e. B) -> B e. On)
70		onelon 2968	. . . . . 6 |- ((B e. On /\ A e. B) -> A e. On)
71		suceloni 3058	. . . . . 6 |- (A e. On -> suc A e. On)
72	70, 71	syl 10	. . . . 5 |- ((B e. On /\ A e. B) -> suc A e. On)
73	69, 72	jca 288	. . . 4 |- ((B e. On /\ A e. B) -> (B e. On /\ suc A e. On))
74		eloni 2954	. . . . . 6 |- (B e. On -> Ord