r1ord - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem r1ord 4665

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

**Assertion**
Ref	Expression
r1ord	⊢ (B ∈ On → (A ∈ B → (R₁ ‘A) ∈ (R₁ ‘B)))

**Proof of Theorem r1ord**
Step	Hyp	Ref	Expression
1		eleq2 1538	. . . . . 6 ⊢ (x = suc A → (A ∈ x ↔ A ∈ suc A))
2		fveq2 3730	. . . . . . 7 ⊢ (x = suc A → (R₁ ‘x) = (R₁ ‘suc A))
3	2	eleq2d 1544	. . . . . 6 ⊢ (x = suc A → ((R₁ ‘A) ∈ (R₁ ‘x) ↔ (R₁ ‘A) ∈ (R₁ ‘suc A)))
4	1, 3	imbi12d 628	. . . . 5 ⊢ (x = suc A → ((A ∈ x → (R₁ ‘A) ∈ (R₁ ‘x)) ↔ (A ∈ suc A → (R₁ ‘A) ∈ (R₁ ‘suc A))))
5		eleq2 1538	. . . . . 6 ⊢ (x = y → (A ∈ x ↔ A ∈ y))
6		fveq2 3730	. . . . . . 7 ⊢ (x = y → (R₁ ‘x) = (R₁ ‘y))
7	6	eleq2d 1544	. . . . . 6 ⊢ (x = y → ((R₁ ‘A) ∈ (R₁ ‘x) ↔ (R₁ ‘A) ∈ (R₁ ‘y)))
8	5, 7	imbi12d 628	. . . . 5 ⊢ (x = y → ((A ∈ x → (R₁ ‘A) ∈ (R₁ ‘x)) ↔ (A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y))))
9		eleq2 1538	. . . . . 6 ⊢ (x = suc y → (A ∈ x ↔ A ∈ suc y))
10		fveq2 3730	. . . . . . 7 ⊢ (x = suc y → (R₁ ‘x) = (R₁ ‘suc y))
11	10	eleq2d 1544	. . . . . 6 ⊢ (x = suc y → ((R₁ ‘A) ∈ (R₁ ‘x) ↔ (R₁ ‘A) ∈ (R₁ ‘suc y)))
12	9, 11	imbi12d 628	. . . . 5 ⊢ (x = suc y → ((A ∈ x → (R₁ ‘A) ∈ (R₁ ‘x)) ↔ (A ∈ suc y → (R₁ ‘A) ∈ (R₁ ‘suc y))))
13		eleq2 1538	. . . . . 6 ⊢ (x = B → (A ∈ x ↔ A ∈ B))
14		fveq2 3730	. . . . . . 7 ⊢ (x = B → (R₁ ‘x) = (R₁ ‘B))
15	14	eleq2d 1544	. . . . . 6 ⊢ (x = B → ((R₁ ‘A) ∈ (R₁ ‘x) ↔ (R₁ ‘A) ∈ (R₁ ‘B)))
16	13, 15	imbi12d 628	. . . . 5 ⊢ (x = B → ((A ∈ x → (R₁ ‘A) ∈ (R₁ ‘x)) ↔ (A ∈ B → (R₁ ‘A) ∈ (R₁ ‘B))))
17		onelon 2978	. . . . . . 7 ⊢ ((suc A ∈ On ⋀ A ∈ suc A) → A ∈ On)
18		r1suc 4662	. . . . . . . 8 ⊢ (A ∈ On → (R₁ ‘suc A) = ℘(R₁ ‘A))
19		fvex 3738	. . . . . . . . 9 ⊢ (R₁ ‘A) ∈ V
20	19	pwid 2412	. . . . . . . 8 ⊢ (R₁ ‘A) ∈ ℘(R₁ ‘A)
21	18, 20	syl5eleqr 1558	. . . . . . 7 ⊢ (A ∈ On → (R₁ ‘A) ∈ (R₁ ‘suc A))
22	17, 21	syl 10	. . . . . 6 ⊢ ((suc A ∈ On ⋀ A ∈ suc A) → (R₁ ‘A) ∈ (R₁ ‘suc A))
23	22	ex 373	. . . . 5 ⊢ (suc A ∈ On → (A ∈ suc A → (R₁ ‘A) ∈ (R₁ ‘suc A)))
24		r1suc 4662	. . . . . . . . . . . . . 14 ⊢ (y ∈ On → (R₁ ‘suc y) = ℘(R₁ ‘y))
25		fvex 3738	. . . . . . . . . . . . . . 15 ⊢ (R₁ ‘y) ∈ V
26	25	pwid 2412	. . . . . . . . . . . . . 14 ⊢ (R₁ ‘y) ∈ ℘(R₁ ‘y)
27	24, 26	syl5eleqr 1558	. . . . . . . . . . . . 13 ⊢ (y ∈ On → (R₁ ‘y) ∈ (R₁ ‘suc y))
28		r1tr 4664	. . . . . . . . . . . . . 14 ⊢ Tr (R₁ ‘suc y)
29		trss 2694	. . . . . . . . . . . . . 14 ⊢ (Tr (R₁ ‘suc y) → ((R₁ ‘y) ∈ (R₁ ‘suc y) → (R₁ ‘y) ⊆ (R₁ ‘suc y)))
30	28, 29	ax-mp 7	. . . . . . . . . . . . 13 ⊢ ((R₁ ‘y) ∈ (R₁ ‘suc y) → (R₁ ‘y) ⊆ (R₁ ‘suc y))
31	27, 30	syl 10	. . . . . . . . . . . 12 ⊢ (y ∈ On → (R₁ ‘y) ⊆ (R₁ ‘suc y))
32	31	sseld 2070	. . . . . . . . . . 11 ⊢ (y ∈ On → ((R₁ ‘A) ∈ (R₁ ‘y) → (R₁ ‘A) ∈ (R₁ ‘suc y)))
33	32	imim2d 25	. . . . . . . . . 10 ⊢ (y ∈ On → ((A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y)) → (A ∈ y → (R₁ ‘A) ∈ (R₁ ‘suc y))))
34		elisset 1820	. . . . . . . . . . . . 13 ⊢ (suc A ∈ On → suc A ∈ V)
35		sucexb 3054	. . . . . . . . . . . . 13 ⊢ (A ∈ V ↔ suc A ∈ V)
36	34, 35	sylibr 200	. . . . . . . . . . . 12 ⊢ (suc A ∈ On → A ∈ V)
37		sucssel 3076	. . . . . . . . . . . 12 ⊢ (A ∈ V → (suc A ⊆ y → A ∈ y))
38	36, 37	syl 10	. . . . . . . . . . 11 ⊢ (suc A ∈ On → (suc A ⊆ y → A ∈ y))
39	38	imp 350	. . . . . . . . . 10 ⊢ ((suc A ∈ On ⋀ suc A ⊆ y) → A ∈ y)
40	33, 39	syl7 23	. . . . . . . . 9 ⊢ (y ∈ On → ((A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y)) → ((suc A ∈ On ⋀ suc A ⊆ y) → (R₁ ‘A) ∈ (R₁ ‘suc y))))
41	40	a1d 12	. . . . . . . 8 ⊢ (y ∈ On → (A ∈ suc y → ((A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y)) → ((suc A ∈ On ⋀ suc A ⊆ y) → (R₁ ‘A) ∈ (R₁ ‘suc y)))))
42	41	com24 37	. . . . . . 7 ⊢ (y ∈ On → ((suc A ∈ On ⋀ suc A ⊆ y) → ((A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y)) → (A ∈ suc y → (R₁ ‘A) ∈ (R₁ ‘suc y)))))
43	42	exp3a 376	. . . . . 6 ⊢ (y ∈ On → (suc A ∈ On → (suc A ⊆ y → ((A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y)) → (A ∈ suc y → (R₁ ‘A) ∈ (R₁ ‘suc y))))))
44	43	imp31 362	. . . . 5 ⊢ (((y ∈ On ⋀ suc A ∈ On) ⋀ suc A ⊆ y) → ((A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y)) → (A ∈ suc y → (R₁ ‘A) ∈ (R₁ ‘suc y))))
45		fveq2 3730	. . . . . . . . . . . . 13 ⊢ (y = suc A → (R₁ ‘y) = (R₁ ‘suc A))
46	45	eleq2d 1544	. . . . . . . . . . . 12 ⊢ (y = suc A → ((R₁ ‘A) ∈ (R₁ ‘y) ↔ (R₁ ‘A) ∈ (R₁ ‘suc A)))
47	46	rcla4ev 1880	. . . . . . . . . . 11 ⊢ ((suc A ∈ x ⋀ (R₁ ‘A) ∈ (R₁ ‘suc A)) → ∃y ∈ x (R₁ ‘A) ∈ (R₁ ‘y))
48		limsuc 3126	. . . . . . . . . . . 12 ⊢ (Lim x → (A ∈ x ↔ suc A ∈ x))
49	48	biimpa 418	. . . . . . . . . . 11 ⊢ ((Lim x ⋀ A ∈ x) → suc A ∈ x)
50		onelon 2978	. . . . . . . . . . . . 13 ⊢ ((x ∈ On ⋀ A ∈ x) → A ∈ On)
51		limord 3034	. . . . . . . . . . . . . 14 ⊢ (Lim x → Ord x)
52		visset 1816	. . . . . . . . . . . . . . 15 ⊢ x ∈ V
53	52	elon 2963	. . . . . . . . . . . . . 14 ⊢ (x ∈ On ↔ Ord x)
54	51, 53	sylibr 200	. . . . . . . . . . . . 13 ⊢ (Lim x → x ∈ On)
55	50, 54	sylan 450	. . . . . . . . . . . 12 ⊢ ((Lim x ⋀ A ∈ x) → A ∈ On)
56	55, 21	syl 10	. . . . . . . . . . 11 ⊢ ((Lim x ⋀ A ∈ x) → (R₁ ‘A) ∈ (R₁ ‘suc A))
57	47, 49, 56	sylanc 473	. . . . . . . . . 10 ⊢ ((Lim x ⋀ A ∈ x) → ∃y ∈ x (R₁ ‘A) ∈ (R₁ ‘y))
58		eliun 2574	. . . . . . . . . 10 ⊢ ((R₁ ‘A) ∈ ∪y ∈ x (R₁ ‘y) ↔ ∃y ∈ x (R₁ ‘A) ∈ (R₁ ‘y))
59	57, 58	sylibr 200	. . . . . . . . 9 ⊢ ((Lim x ⋀ A ∈ x) → (R₁ ‘A) ∈ ∪y ∈ x (R₁ ‘y))
60		r1lim 4663	. . . . . . . . . . . 12 ⊢ ((x ∈ V ⋀ Lim x) → (R₁ ‘x) = ∪y ∈ x (R₁ ‘y))
61	52, 60	mpan 697	. . . . . . . . . . 11 ⊢ (Lim x → (R₁ ‘x) = ∪y ∈ x (R₁ ‘y))
62	61	eleq2d 1544	. . . . . . . . . 10 ⊢ (Lim x → ((R₁ ‘A) ∈ (R₁ ‘x) ↔ (R₁ ‘A) ∈ ∪y ∈ x (R₁ ‘y)))
63	62	adantr 391	. . . . . . . . 9 ⊢ ((Lim x ⋀ A ∈ x) → ((R₁ ‘A) ∈ (R₁ ‘x) ↔ (R₁ ‘A) ∈ ∪y ∈ x (R₁ ‘y)))
64	59, 63	mpbird 196	. . . . . . . 8 ⊢ ((Lim x ⋀ A ∈ x) → (R₁ ‘A) ∈ (R₁ ‘x))
65	64	ex 373	. . . . . . 7 ⊢ (Lim x → (A ∈ x → (R₁ ‘A) ∈ (R₁ ‘x)))
66	65	ad2antrr 406	. . . . . 6 ⊢ (((Lim x ⋀ suc A ∈ On) ⋀ suc A ⊆ x) → (A ∈ x → (R₁ ‘A) ∈ (R₁ ‘x)))
67	66	a1d 12	. . . . 5 ⊢ (((Lim x ⋀ suc A ∈ On) ⋀ suc A ⊆ x) → (∀y ∈ x (suc A ⊆ y → (A ∈ y → (R₁ ‘A) ∈ (R₁ ‘y))) → (A ∈ x → (R₁ ‘A) ∈ (R₁ ‘x))))
68	4, 8, 12, 16, 23, 44, 67	tfindsg 3168	. . . 4 ⊢ (((B ∈ On ⋀ suc A ∈ On) ⋀ suc A ⊆ B) → (A ∈ B → (R₁ ‘A) ∈ (R₁ ‘B)))
69		pm3.26 319	. . . . 5 ⊢ ((B ∈ On ⋀ A ∈ B) → B ∈ On)
70		onelon 2978	. . . . . 6 ⊢ ((B ∈ On ⋀ A ∈ B) → A ∈ On)
71		suceloni 3068	. . . . . 6 ⊢ (A ∈ On → suc A ∈ On)
72	70, 71	syl 10	. . . . 5 ⊢ ((B ∈ On ⋀ A ∈ B) → suc A ∈ On)
73	69, 72	jca 288	. . . 4 ⊢ ((B ∈ On ⋀ A ∈ B) → (B ∈ On ⋀ suc A ∈ On))
74		eloni 2964	. . . . . 6 ⊢ (B ∈ On → Ord B)
75		ordsucss 3075	. . . . . 6 ⊢ (Ord B → (A ∈ B → suc A ⊆ B))
76	74, 75	syl 10	. . . . 5 ⊢ (B ∈ On → (A ∈ B → suc A ⊆ B))
77	76	imp 350	. . . 4 ⊢ ((B ∈ On ⋀ A ∈ B) → suc A ⊆ B)
78	68, 73, 77	sylanc 473	. . 3 ⊢ ((B ∈ On ⋀ A ∈ B) → (A ∈ B → (R₁ ‘A) ∈ (R₁ ‘B)))
79	78	ex 373	. 2 ⊢ (B ∈ On → (A ∈ B → (A ∈ B → (R₁ ‘A) ∈ (R₁ ‘B))))
80	79	pm2.43d 65	1 ⊢ (B ∈ On → (A ∈ B → (R₁ ‘A) ∈ (R₁ ‘B)))

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 = wceq 958 ∈ wcel 960 ∀wral 1648 ∃wrex 1649 Vcvv 1814 ⊆ wss 2050 ℘cpw 2405 ∪ciun 2570 Tr wtr 2685 Ord word 2953 Oncon0 2954 Lim wlim 2955 suc csuc 2956 ‘cfv 3188 R₁cr1 4651

This theorem is referenced by: r1ord2 4666

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-ral 1652 df-rex 1653 df-rab 1655 df-v 1815 df-sbc 1945 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-fv 3204 df-rdg 3938 df-r1 4653