Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

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 ∈ On → (A ∈ B → (R₁ ‘A) ∈ (R₁ ‘B)))

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

Colors of variables: wff set class

Syntax hints: → wi 2 ↔ wb 127 ∧ wa 196 = weq 797 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 Vcvv 1348 ⊆ wss 1487 ℘cpw 1798 ∪ciun 1994 Tr wtr 2041 Ord word 2198 Oncon0 2199 Lim wlim 2200 suc csuc 2201 ‘cfv 2422 R₁cr1 3485

This theorem is referenced by: r1ord2 3500

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438 df-rdg 2970 df-r1 3487

metamath.org