Theorem r1ord 3499

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 1150	. . . . . 6 |- (x = suc A -> (A e. x <-> A e. suc A))
2		fveq2 2832	. . . . . . 7 |- (x = suc A -> (R1` x) = (R1` suc A))
3	2	eleq2d 1156	. . . . . 6 |- (x = suc A -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` suc A)))
4	1, 3	imbi12d 474	. . . . 5 |- (x = suc A -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. suc A -> (R1` A) e. (R1` suc A))))
5		eleq2 1150	. . . . . 6 |- (x = y -> (A e. x <-> A e. y))
6		fveq2 2832	. . . . . . 7 |- (x = y -> (R1` x) = (R1` y))
7	6	eleq2d 1156	. . . . . 6 |- (x = y -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` y)))
8	5, 7	imbi12d 474	. . . . 5 |- (x = y -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. y -> (R1` A) e. (R1` y))))
9		eleq2 1150	. . . . . 6 |- (x = suc y -> (A e. x <-> A e. suc y))
10		fveq2 2832	. . . . . . 7 |- (x = suc y -> (R1` x) = (R1` suc y))
11	10	eleq2d 1156	. . . . . 6 |- (x = suc y -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` suc y)))
12	9, 11	imbi12d 474	. . . . 5 |- (x = suc y -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. suc y -> (R1` A) e. (R1` suc y))))
13		eleq2 1150	. . . . . 6 |- (x = B -> (A e. x <-> A e. B))
14		fveq2 2832	. . . . . . 7 |- (x = B -> (R1` x) = (R1` B))
15	14	eleq2d 1156	. . . . . 6 |- (x = B -> ((R1` A) e. (R1` x) <-> (R1` A) e. (R1` B)))
16	13, 15	imbi12d 474	. . . . 5 |- (x = B -> ((A e. x -> (R1` A) e. (R1` x)) <-> (A e. B -> (R1` A) e. (R1` B))))
17		onelon 2223	. . . . . . 7 |- ((suc A e. On /\ A e. suc A) -> A e. On)
18		fvex 2838	. . . . . . . . 9 |- (R1` A) e. V
19	18	pwid 1805	. . . . . . . 8 |- (R1` A) e. P~(R1` A)
20		r1suc 3496	. . . . . . . . 9 |- (A e. On -> (R1` suc A) = P~(R1` A))
21	20	eleq2d 1156	. . . . . . . 8 |- (A e. On -> ((R1` A) e. (R1` suc A) <-> (R1` A) e. P~(R1` A)))
22	19, 21	mpbiri 169	. . . . . . 7 |- (A e. On -> (R1` A) e. (R1` suc A))
23	17, 22	syl 12	. . . . . 6 |- ((suc A e. On /\ A e. suc A) -> (R1` A) e. (R1` suc A))
24	23	exp 291	. . . . 5 |- (suc A e. On -> (A e. suc A -> (R1` A) e. (R1` suc A)))
25		fvex 2838	. . . . . . . . . . . . . . 15 |- (R1` y) e. V
26	25	pwid 1805	. . . . . . . . . . . . . 14 |- (R1` y) e. P~(R1` y)
27		r1suc 3496	. . . . . . . . . . . . . . 15 |- (y e. On -> (R1` suc y) = P~(R1` y))
28	27	eleq2d 1156	. . . . . . . . . . . . . 14 |- (y e. On -> ((R1` y) e. (R1` suc y) <-> (R1` y) e. P~(R1` y)))
29	26, 28	mpbiri 169	. . . . . . . . . . . . 13 |- (y e. On -> (R1` y) e. (R1` suc y))
30		r1tr 3498	. . . . . . . . . . . . . 14 |- Tr (R1` suc y)
31		trss 2050	. . . . . . . . . . . . . 14 |- (Tr (R1` suc y) -> ((R1` y) e. (R1` suc y) -> (R1` y) (_ (R1` suc y)))
32	30, 31	ax-mp 6	. . . . . . . . . . . . 13 |- ((R1` y) e. (R1` suc y) -> (R1` y) (_ (R1` suc y))
33	29, 32	syl 12	. . . . . . . . . . . 12 |- (y e. On -> (R1` y) (_ (R1` suc y))
34	33	sseld 1506	. . . . . . . . . . 11 |- (y e. On -> ((R1` A) e. (R1` y) -> (R1` A) e. (R1` suc y)))
35	34	syl3d 26	. . . . . . . . . 10 |- (y e. On -> ((A e. y -> (R1` A) e. (R1` y)) -> (A e. y -> (R1` A) e. (R1` suc y))))
36		elisset 1354	. . . . . . . . . . . . 13 |- (suc A e. On -> suc A e. V)
37		sucexb 2301	. . . . . . . . . . . . 13 |- (A e. V <-> suc A e. V)
38	36, 37	sylibr 175	. . . . . . . . . . . 12 |- (suc A e. On -> A e. V)
39		sucssel 2321	. . . . . . . . . . . 12 |- (A e. V -> (suc A (_ y -> A e. y))
40	38, 39	syl 12	. . . . . . . . . . 11 |- (suc A e. On -> (suc A (_ y -> A e. y))
41	40	imp 277	. . . . . . . . . 10 |- ((suc A e. On /\ suc A (_ y) -> A e. y)
42	35, 41	syl7 24	. . . . . . . . 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))))
43	42	a1d 14	. . . . . . . 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)))))
44	43	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)))))
45	44	exp3a 292	. . . . . 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))))))
46	45	imp31 280	. . . . 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))))
47		fveq2 2832	. . . . . . . . . . . . 13 |- (y = suc A -> (R1` y) = (R1` suc A))
48	47	eleq2d 1156	. . . . . . . . . . . 12 |- (y = suc A -> ((R1` A) e. (R1` y) <-> (R1` A) e. (R1` suc A)))
49	48	rcla4ev 1403	. . . . . . . . . . 11 |- ((suc A e. x /\ (R1` A) e. (R1` suc A)) -> E.y e. x (R1` A) e. (R1` y))
50		limsuc 2361	. . . . . . . . . . . 12 |- (Lim x -> (A e. x <-> suc A e. x))
51	50	biimpa 324	. . . . . . . . . . 11 |- ((Lim x /\ A e. x) -> suc A e. x)
52		onelon 2223	. . . . . . . . . . . . 13 |- ((x e. On /\ A e. x) -> A e. On)
53		limord 2283	. . . . . . . . . . . . . 14 |- (Lim x -> Ord x)
54		visset 1350	. . . . . . . . . . . . . . 15 |- x e. V
55	54	elon 2208	. . . . . . . . . . . . . 14 |- (x e. On <-> Ord x)
56	53, 55	sylibr 175	. . . . . . . . . . . . 13 |- (Lim x -> x e. On)
57	52, 56	sylan 343	. . . . . . . . . . . 12 |- ((Lim x /\ A e. x) -> A e. On)
58	57, 22	syl 12	. . . . . . . . . . 11 |- ((Lim x /\ A e. x) -> (R1` A) e. (R1` suc A))
59	49, 51, 58	sylanc 361	. . . . . . . . . 10 |- ((Lim x /\ A e. x) -> E.y e. x (R1` A) e. (R1` y))
60		eliun 1998	. . . . . . . . . 10 |- ((R1` A) e. U.y e. x (R1` y) <-> E.y e. x (R1` A) e. (R1` y))
61	59, 60	sylibr 175	. . . . . . . . 9 |- ((Lim x /\ A e. x) -> (R1` A) e. U.y e. x (R1` y))
62		r1lim 3497	. . . . . . . . . . . 12 |- ((x e. V /\ Lim x) -> (R1` x) = U.y e. x (R1` y))
63	54, 62	mpan 518	. . . . . . . . . . 11 |- (Lim x -> (R1` x) = U.y e. x (R1` y))
64	63	eleq2d 1156	. . . . . . . . . 10 |- (Lim x -> ((R1` A) e. (R1` x) <-> (R1` A) e. U.y e. x (R1` y)))
65	64	adantr 306	. . . . . . . . 9 |- ((Lim x /\ A e. x) -> ((R1` A) e. (R1` x) <-> (R1` A) e. U.y e. x (R1` y)))
66	61, 65	mpbird 171	. . . . . . . 8 |- ((Lim x /\ A e. x) -> (R1` A) e. (R1` x))
67	66	exp 291	. . . . . . 7 |- (Lim x -> (A e. x -> (R1` A) e. (R1` x)))
68	67	ad2antll 320	. . . . . 6 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (A e. x -> (R1` A) e. (R1` x)))
69	68	a1d 14	. . . . 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))))
70	4, 8, 12, 16, 24, 46, 69	tfindsg 2402	. . . 4 |- (((B e. On /\ suc A e. On) /\ suc A (_ B) -> (A e. B -> (R1` A) e. (R1` B)))
71		pm3.26 256	. . . . 5 |- ((B e. On /\ A e. B) -> B e. On)
72		onelon 2223	. . . . . 6 |- ((B e. On /\ A e. B) -> A e. On)
73		suceloni 2314	. . . . . 6 |- (A e. On -> suc A e. On)
74	72, 73	syl 12	. . . . 5 |- ((B e. On /\ A e. B) -> suc A e. On)
75	71, 74	jca 236	. . . 4 |- ((B e. On /\ A e. B) -> (B e. On /\ suc A e. On))
76		eloni 2209	. . . . . 6 |- (B e. On -> Ord B)
77		ordsucss 2320	. . . . . 6 |- (Ord B -> (A e. B ->