r1val1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem r1val1 4668

Description: The value of the cumulative hierarchy of sets function expressed recursively. Theorem 7Q of [Enderton] p. 202.

**Assertion**
Ref	Expression
r1val1	⊢ (A ∈ On → (R₁ ‘A) = ∪x ∈ A ℘(R₁ ‘x))

Distinct variable group: x,A

**Proof of Theorem r1val1**
Step	Hyp	Ref	Expression
1		onzsl 3123	. . 3 ⊢ (A ∈ On ↔ (A = ∅ ⋁ ∃x ∈ On A = suc x ⋁ (A ∈ V ⋀ Lim A)))
2		0ss 2305	. . . . 5 ⊢ ∅ ⊆ ∪x ∈ A ℘(R₁ ‘x)
3		fveq2 3730	. . . . . . 7 ⊢ (A = ∅ → (R₁ ‘A) = (R₁ ‘∅))
4		r10 4661	. . . . . . 7 ⊢ (R₁ ‘∅) = ∅
5	3, 4	syl6eq 1526	. . . . . 6 ⊢ (A = ∅ → (R₁ ‘A) = ∅)
6	5	sseq1d 2091	. . . . 5 ⊢ (A = ∅ → ((R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x) ↔ ∅ ⊆ ∪x ∈ A ℘(R₁ ‘x)))
7	2, 6	mpbiri 194	. . . 4 ⊢ (A = ∅ → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
8		ax-17 973	. . . . . 6 ⊢ (y ∈ (R₁ ‘A) → ∀x y ∈ (R₁ ‘A))
9		hbiu1 2588	. . . . . 6 ⊢ (y ∈ ∪x ∈ A ℘(R₁ ‘x) → ∀x y ∈ ∪x ∈ A ℘(R₁ ‘x))
10	8, 9	hbss 2065	. . . . 5 ⊢ ((R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x) → ∀x(R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
11		fveq2 3730	. . . . . . . 8 ⊢ (A = suc x → (R₁ ‘A) = (R₁ ‘suc x))
12		r1suc 4662	. . . . . . . 8 ⊢ (x ∈ On → (R₁ ‘suc x) = ℘(R₁ ‘x))
13	11, 12	sylan9eqr 1532	. . . . . . 7 ⊢ ((x ∈ On ⋀ A = suc x) → (R₁ ‘A) = ℘(R₁ ‘x))
14		visset 1816	. . . . . . . . . . 11 ⊢ x ∈ V
15	14	sucid 3057	. . . . . . . . . 10 ⊢ x ∈ suc x
16		eleq2 1538	. . . . . . . . . 10 ⊢ (A = suc x → (x ∈ A ↔ x ∈ suc x))
17	15, 16	mpbiri 194	. . . . . . . . 9 ⊢ (A = suc x → x ∈ A)
18		ssiun2 2597	. . . . . . . . 9 ⊢ (x ∈ A → ℘(R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
19	17, 18	syl 10	. . . . . . . 8 ⊢ (A = suc x → ℘(R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
20	19	adantl 390	. . . . . . 7 ⊢ ((x ∈ On ⋀ A = suc x) → ℘(R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
21	13, 20	eqsstrd 2098	. . . . . 6 ⊢ ((x ∈ On ⋀ A = suc x) → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
22	21	ex 373	. . . . 5 ⊢ (x ∈ On → (A = suc x → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x)))
23	10, 22	r19.23ai 1745	. . . 4 ⊢ (∃x ∈ On A = suc x → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
24		r1lim 4663	. . . . 5 ⊢ ((A ∈ V ⋀ Lim A) → (R₁ ‘A) = ∪x ∈ A (R₁ ‘x))
25		ordelon 2977	. . . . . . . . . 10 ⊢ ((Ord A ⋀ x ∈ A) → x ∈ On)
26		limord 3034	. . . . . . . . . 10 ⊢ (Lim A → Ord A)
27	25, 26	sylan 450	. . . . . . . . 9 ⊢ ((Lim A ⋀ x ∈ A) → x ∈ On)
28		sucelon 3074	. . . . . . . . . . 11 ⊢ (x ∈ On ↔ suc x ∈ On)
29		r1ord2 4666	. . . . . . . . . . . 12 ⊢ (suc x ∈ On → (x ∈ suc x → (R₁ ‘x) ⊆ (R₁ ‘suc x)))
30	15, 29	mpi 44	. . . . . . . . . . 11 ⊢ (suc x ∈ On → (R₁ ‘x) ⊆ (R₁ ‘suc x))
31	28, 30	sylbi 199	. . . . . . . . . 10 ⊢ (x ∈ On → (R₁ ‘x) ⊆ (R₁ ‘suc x))
32	31, 12	sseqtrd 2100	. . . . . . . . 9 ⊢ (x ∈ On → (R₁ ‘x) ⊆ ℘(R₁ ‘x))
33	27, 32	syl 10	. . . . . . . 8 ⊢ ((Lim A ⋀ x ∈ A) → (R₁ ‘x) ⊆ ℘(R₁ ‘x))
34	33	r19.21aiva 1717	. . . . . . 7 ⊢ (Lim A → ∀x ∈ A (R₁ ‘x) ⊆ ℘(R₁ ‘x))
35		ss2iun 2581	. . . . . . 7 ⊢ (∀x ∈ A (R₁ ‘x) ⊆ ℘(R₁ ‘x) → ∪x ∈ A (R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
36	34, 35	syl 10	. . . . . 6 ⊢ (Lim A → ∪x ∈ A (R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
37	36	adantl 390	. . . . 5 ⊢ ((A ∈ V ⋀ Lim A) → ∪x ∈ A (R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
38	24, 37	eqsstrd 2098	. . . 4 ⊢ ((A ∈ V ⋀ Lim A) → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
39	7, 23, 38	3jaoi 889	. . 3 ⊢ ((A = ∅ ⋁ ∃x ∈ On A = suc x ⋁ (A ∈ V ⋀ Lim A)) → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
40	1, 39	sylbi 199	. 2 ⊢ (A ∈ On → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
41		onelon 2978	. . . . . 6 ⊢ ((A ∈ On ⋀ x ∈ A) → x ∈ On)
42	41, 12	syl 10	. . . . 5 ⊢ ((A ∈ On ⋀ x ∈ A) → (R₁ ‘suc x) = ℘(R₁ ‘x))
43		r1ord3 4667	. . . . . 6 ⊢ ((suc x ∈ On ⋀ A ∈ On) → (suc x ⊆ A → (R₁ ‘suc x) ⊆ (R₁ ‘A)))
44	41, 28	sylib 198	. . . . . . 7 ⊢ ((A ∈ On ⋀ x ∈ A) → suc x ∈ On)
45		pm3.26 319	. . . . . . 7 ⊢ ((A ∈ On ⋀ x ∈ A) → A ∈ On)
46	44, 45	jca 288	. . . . . 6 ⊢ ((A ∈ On ⋀ x ∈ A) → (suc x ∈ On ⋀ A ∈ On))
47		eloni 2964	. . . . . . . 8 ⊢ (A ∈ On → Ord A)
48		ordsucss 3075	. . . . . . . 8 ⊢ (Ord A → (x ∈ A → suc x ⊆ A))
49	47, 48	syl 10	. . . . . . 7 ⊢ (A ∈ On → (x ∈ A → suc x ⊆ A))
50	49	imp 350	. . . . . 6 ⊢ ((A ∈ On ⋀ x ∈ A) → suc x ⊆ A)
51	43, 46, 50	sylc 68	. . . . 5 ⊢ ((A ∈ On ⋀ x ∈ A) → (R₁ ‘suc x) ⊆ (R₁ ‘A))
52	42, 51	eqsstr3d 2099	. . . 4 ⊢ ((A ∈ On ⋀ x ∈ A) → ℘(R₁ ‘x) ⊆ (R₁ ‘A))
53	52	r19.21aiva 1717	. . 3 ⊢ (A ∈ On → ∀x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A))
54		iunss 2595	. . 3 ⊢ (∪x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A) ↔ ∀x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A))
55	53, 54	sylibr 200	. 2 ⊢ (A ∈ On → ∪x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A))
56	40, 55	eqssd 2082	1 ⊢ (A ∈ On → (R₁ ‘A) = ∪x ∈ A ℘(R₁ ‘x))

Colors of variables: wff set class

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

This theorem is referenced by: r1val3 4689

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