Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem r1pwcl 3530

Description: The cumulative hierarchy of a limit ordinal is closed under powerset. (Contributed by Raph Levien, 29-May-04.)

**Assertion**
Ref	Expression
r1pwcl	⊢ (Lim B → (A ∈ (R₁ ‘B) ↔ ℘A ∈ (R₁ ‘B)))

**Proof of Theorem r1pwcl**
Step	Hyp	Ref	Expression
1		r1lim 3497	. . . . . . 7 ⊢ ((B ∈ V ∧ Lim B) → (R₁ ‘B) = ∪x ∈ B (R₁ ‘x))
2	1	eleq2d 1156	. . . . . 6 ⊢ ((B ∈ V ∧ Lim B) → (A ∈ (R₁ ‘B) ↔ A ∈ ∪x ∈ B (R₁ ‘x)))
3		eliun 1998	. . . . . 6 ⊢ (A ∈ ∪x ∈ B (R₁ ‘x) ↔ ∃x ∈ B A ∈ (R₁ ‘x))
4	2, 3	syl6bb 414	. . . . 5 ⊢ ((B ∈ V ∧ Lim B) → (A ∈ (R₁ ‘B) ↔ ∃x ∈ B A ∈ (R₁ ‘x)))
5		onelon 2223	. . . . . . . 8 ⊢ ((B ∈ On ∧ x ∈ B) → x ∈ On)
6		limelon 2286	. . . . . . . 8 ⊢ ((B ∈ V ∧ Lim B) → B ∈ On)
7	5, 6	sylan 343	. . . . . . 7 ⊢ (((B ∈ V ∧ Lim B) ∧ x ∈ B) → x ∈ On)
8		r1pw 3529	. . . . . . 7 ⊢ (x ∈ On → (A ∈ (R₁ ‘x) ↔ ℘A ∈ (R₁ ‘suc x)))
9	7, 8	syl 12	. . . . . 6 ⊢ (((B ∈ V ∧ Lim B) ∧ x ∈ B) → (A ∈ (R₁ ‘x) ↔ ℘A ∈ (R₁ ‘suc x)))
10	9	birexdva 1216	. . . . 5 ⊢ ((B ∈ V ∧ Lim B) → (∃x ∈ B A ∈ (R₁ ‘x) ↔ ∃x ∈ B ℘A ∈ (R₁ ‘suc x)))
11		limsuc 2361	. . . . . . . . . . . 12 ⊢ (Lim B → (x ∈ B ↔ suc x ∈ B))
12	11	anbi1d 469	. . . . . . . . . . 11 ⊢ (Lim B → ((x ∈ B ∧ ℘A ∈ (R₁ ‘suc x)) ↔ (suc x ∈ B ∧ ℘A ∈ (R₁ ‘suc x))))
13		visset 1350	. . . . . . . . . . . . 13 ⊢ x ∈ V
14	13	sucex 2303	. . . . . . . . . . . 12 ⊢ suc x ∈ V
15		eleq1 1149	. . . . . . . . . . . . 13 ⊢ (y = suc x → (y ∈ B ↔ suc x ∈ B))
16		fveq2 2832	. . . . . . . . . . . . . 14 ⊢ (y = suc x → (R₁ ‘y) = (R₁ ‘suc x))
17	16	eleq2d 1156	. . . . . . . . . . . . 13 ⊢ (y = suc x → (℘A ∈ (R₁ ‘y) ↔ ℘A ∈ (R₁ ‘suc x)))
18	15, 17	anbi12d 476	. . . . . . . . . . . 12 ⊢ (y = suc x → ((y ∈ B ∧ ℘A ∈ (R₁ ‘y)) ↔ (suc x ∈ B ∧ ℘A ∈ (R₁ ‘suc x))))
19	14, 18	cla4ev 1401	. . . . . . . . . . 11 ⊢ ((suc x ∈ B ∧ ℘A ∈ (R₁ ‘suc x)) → ∃y(y ∈ B ∧ ℘A ∈ (R₁ ‘y)))
20	12, 19	syl6bi 187	. . . . . . . . . 10 ⊢ (Lim B → ((x ∈ B ∧ ℘A ∈ (R₁ ‘suc x)) → ∃y(y ∈ B ∧ ℘A ∈ (R₁ ‘y))))
21	20	19.23adv 954	. . . . . . . . 9 ⊢ (Lim B → (∃x(x ∈ B ∧ ℘A ∈ (R₁ ‘suc x)) → ∃y(y ∈ B ∧ ℘A ∈ (R₁ ‘y))))
22		df-rex 1206	. . . . . . . . 9 ⊢ (∃x ∈ B ℘A ∈ (R₁ ‘suc x) ↔ ∃x(x ∈ B ∧ ℘A ∈ (R₁ ‘suc x)))
23		df-rex 1206	. . . . . . . . 9 ⊢ (∃y ∈ B ℘A ∈ (R₁ ‘y) ↔ ∃y(y ∈ B ∧ ℘A ∈ (R₁ ‘y)))
24	21, 22, 23	3imtr4g 426	. . . . . . . 8 ⊢ (Lim B → (∃x ∈ B ℘A ∈ (R₁ ‘suc x) → ∃y ∈ B ℘A ∈ (R₁ ‘y)))
25		fveq2 2832	. . . . . . . . . 10 ⊢ (x = y → (R₁ ‘x) = (R₁ ‘y))
26	25	eleq2d 1156	. . . . . . . . 9 ⊢ (x = y → (℘A ∈ (R₁ ‘x) ↔ ℘A ∈ (R₁ ‘y)))
27	26	cbvrexv 1334	. . . . . . . 8 ⊢ (∃x ∈ B ℘A ∈ (R₁ ‘x) ↔ ∃y ∈ B ℘A ∈ (R₁ ‘y))
28	24, 27	syl6ibr 186	. . . . . . 7 ⊢ (Lim B → (∃x ∈ B ℘A ∈ (R₁ ‘suc x) → ∃x ∈ B ℘A ∈ (R₁ ‘x)))
29	28	adantl 305	. . . . . 6 ⊢ ((B ∈ V ∧ Lim B) → (∃x ∈ B ℘A ∈ (R₁ ‘suc x) → ∃x ∈ B ℘A ∈ (R₁ ‘x)))
30	7	exp 291	. . . . . . . 8 ⊢ ((B ∈ V ∧ Lim B) → (x ∈ B → x ∈ On))
31		sssucid 2300	. . . . . . . . . . . 12 ⊢ x ⊆ suc x
32		r1ord3 3501	. . . . . . . . . . . 12 ⊢ ((x ∈ On ∧ suc x ∈ On) → (x ⊆ suc x → (R₁ ‘x) ⊆ (R₁ ‘suc x)))
33	31, 32	mpi 44	. . . . . . . . . . 11 ⊢ ((x ∈ On ∧ suc x ∈ On) → (R₁ ‘x) ⊆ (R₁ ‘suc x))
34		sucelon 2319	. . . . . . . . . . 11 ⊢ (x ∈ On ↔ suc x ∈ On)
35	33, 34	sylan2b 347	. . . . . . . . . 10 ⊢ ((x ∈ On ∧ x ∈ On) → (R₁ ‘x) ⊆ (R₁ ‘suc x))
36	35	anidms 332	. . . . . . . . 9 ⊢ (x ∈ On → (R₁ ‘x) ⊆ (R₁ ‘suc x))
37	36	sseld 1506	. . . . . . . 8 ⊢ (x ∈ On → (℘A ∈ (R₁ ‘x) → ℘A ∈ (R₁ ‘suc x)))
38	30, 37	syl6 23	. . . . . . 7 ⊢ ((B ∈ V ∧ Lim B) → (x ∈ B → (℘A ∈ (R₁ ‘x) → ℘A ∈ (R₁ ‘suc x))))
39	38	r19.22dv 1278	. . . . . 6 ⊢ ((B ∈ V ∧ Lim B) → (∃x ∈ B ℘A ∈ (R₁ ‘x) → ∃x ∈ B ℘A ∈ (R₁ ‘suc x)))
40	29, 39	impbid 397	. . . . 5 ⊢ ((B ∈ V ∧ Lim B) → (∃x ∈ B ℘A ∈ (R₁ ‘suc x) ↔ ∃x ∈ B ℘A ∈ (R₁ ‘x)))
41	4, 10, 40	3bitrd 422	. . . 4 ⊢ ((B ∈ V ∧ Lim B) → (A ∈ (R₁ ‘B) ↔ ∃x ∈ B ℘A ∈ (R₁ ‘x)))
42	1	eleq2d 1156	. . . . 5 ⊢ ((B ∈ V ∧ Lim B) → (℘A ∈ (R₁ ‘B) ↔ ℘A ∈ ∪x ∈ B (R₁ ‘x)))
43		eliun 1998	. . . . 5 ⊢ (℘A ∈ ∪x ∈ B (R₁ ‘x) ↔ ∃x ∈ B ℘A ∈ (R₁ ‘x))
44	42, 43	syl6bb 414	. . . 4 ⊢ ((B ∈ V ∧ Lim B) → (℘A ∈ (R₁ ‘B) ↔ ∃x ∈ B ℘A ∈ (R₁ ‘x)))
45	41, 44	bitr4d 409	. . 3 ⊢ ((B ∈ V ∧ Lim B) → (A ∈ (R₁ ‘B) ↔ ℘A ∈ (R₁ ‘B)))
46	45	exp 291	. 2 ⊢ (B ∈ V → (Lim B → (A ∈ (R₁ ‘B) ↔ ℘A ∈ (R₁ ‘B))))
47		n0i 1712	. . . . 5 ⊢ (A ∈ (R₁ ‘B) → ¬ (R₁ ‘B) = ∅)
48		fvprc 2829	. . . . 5 ⊢ (¬ B ∈ V → (R₁ ‘B) = ∅)
49	47, 48	nsyl2 103	. . . 4 ⊢ (A ∈ (R₁ ‘B) → B ∈ V)
50		n0i 1712	. . . . 5 ⊢ (℘A ∈ (R₁ ‘B) → ¬ (R₁ ‘B) = ∅)
51	50, 48	nsyl2 103	. . . 4 ⊢ (℘A ∈ (R₁ ‘B) → B ∈ V)
52	49, 51	pm5.21ni 503	. . 3 ⊢ (¬ B ∈ V → (A ∈ (R₁ ‘B) ↔ ℘A ∈ (R₁ ‘B)))
53	52	a1d 14	. 2 ⊢ (¬ B ∈ V → (Lim B → (A ∈ (R₁ ‘B) ↔ ℘A ∈ (R₁ ‘B))))
54	46, 53	pm2.61i 110	1 ⊢ (Lim B → (A ∈ (R₁ ‘B) ↔ ℘A ∈ (R₁ ‘B)))

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∧ wa 196 ∃wex 678 = weq 797 = wceq 1091 ∈ wcel 1092 ∃wrex 1202 Vcvv 1348 ⊆ wss 1487 ∅c0 1707 ℘cpw 1798 ∪ciun 1994 Oncon0 2199 Lim wlim 2200 suc csuc 2201 ‘cfv 2422 R₁cr1 3485

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 ax-reg 1078 ax-inf 1079

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-ne 1192 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-pss 1494 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-int 1966 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-om 2373 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-f 2434 df-f1 2435 df-fv 2438 df-rdg 2970 df-r1 3487 df-rank 3488

metamath.org