Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem r1val1 3502

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(s): x,A

**Proof of Theorem r1val1**
Step	Hyp	Ref	Expression
1		onzsl 2367	. . 3 ⊢ (A ∈ On ↔ (A = ∅ ∨ ∃x ∈ On A = suc x ∨ (A ∈ V ∧ Lim A)))
2		0ss 1725	. . . . 5 ⊢ ∅ ⊆ ∪x ∈ A ℘(R₁ ‘x)
3		fveq2 2832	. . . . . . 7 ⊢ (A = ∅ → (R₁ ‘A) = (R₁ ‘∅))
4		r10 3495	. . . . . . 7 ⊢ (R₁ ‘∅) = ∅
5	3, 4	syl6eq 1140	. . . . . 6 ⊢ (A = ∅ → (R₁ ‘A) = ∅)
6	5	sseq1d 1527	. . . . 5 ⊢ (A = ∅ → ((R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x) ↔ ∅ ⊆ ∪x ∈ A ℘(R₁ ‘x)))
7	2, 6	mpbiri 169	. . . 4 ⊢ (A = ∅ → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
8		ax-17 925	. . . . . 6 ⊢ (y ∈ (R₁ ‘A) → ∀x y ∈ (R₁ ‘A))
9		hbiu1 2012	. . . . . 6 ⊢ (y ∈ ∪x ∈ A ℘(R₁ ‘x) → ∀x y ∈ ∪x ∈ A ℘(R₁ ‘x))
10	8, 9	hbss 1501	. . . . 5 ⊢ ((R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x) → ∀x(R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
11		fveq2 2832	. . . . . . . 8 ⊢ (A = suc x → (R₁ ‘A) = (R₁ ‘suc x))
12		r1suc 3496	. . . . . . . 8 ⊢ (x ∈ On → (R₁ ‘suc x) = ℘(R₁ ‘x))
13	11, 12	sylan9eqr 1145	. . . . . . 7 ⊢ ((x ∈ On ∧ A = suc x) → (R₁ ‘A) = ℘(R₁ ‘x))
14		visset 1350	. . . . . . . . . . 11 ⊢ x ∈ V
15	14	sucid 2304	. . . . . . . . . 10 ⊢ x ∈ suc x
16		eleq2 1150	. . . . . . . . . 10 ⊢ (A = suc x → (x ∈ A ↔ x ∈ suc x))
17	15, 16	mpbiri 169	. . . . . . . . 9 ⊢ (A = suc x → x ∈ A)
18		ssiun2 2019	. . . . . . . . 9 ⊢ (x ∈ A → ℘(R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
19	17, 18	syl 12	. . . . . . . 8 ⊢ (A = suc x → ℘(R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
20	19	adantl 305	. . . . . . 7 ⊢ ((x ∈ On ∧ A = suc x) → ℘(R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
21	13, 20	eqsstrd 1534	. . . . . 6 ⊢ ((x ∈ On ∧ A = suc x) → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
22	21	exp 291	. . . . 5 ⊢ (x ∈ On → (A = suc x → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x)))
23	10, 22	r19.23ai 1283	. . . 4 ⊢ (∃x ∈ On A = suc x → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
24		r1lim 3497	. . . . 5 ⊢ ((A ∈ V ∧ Lim A) → (R₁ ‘A) = ∪x ∈ A (R₁ ‘x))
25		ordelon 2222	. . . . . . . . . . 11 ⊢ ((Ord A ∧ x ∈ A) → x ∈ On)
26		limord 2283	. . . . . . . . . . 11 ⊢ (Lim A → Ord A)
27	25, 26	sylan 343	. . . . . . . . . 10 ⊢ ((Lim A ∧ x ∈ A) → x ∈ On)
28		sucelon 2319	. . . . . . . . . . . 12 ⊢ (x ∈ On ↔ suc x ∈ On)
29		r1ord2 3500	. . . . . . . . . . . . 13 ⊢ (suc x ∈ On → (x ∈ suc x → (R₁ ‘x) ⊆ (R₁ ‘suc x)))
30	15, 29	mpi 44	. . . . . . . . . . . 12 ⊢ (suc x ∈ On → (R₁ ‘x) ⊆ (R₁ ‘suc x))
31	28, 30	sylbi 174	. . . . . . . . . . 11 ⊢ (x ∈ On → (R₁ ‘x) ⊆ (R₁ ‘suc x))
32	31, 12	sseqtrd 1536	. . . . . . . . . 10 ⊢ (x ∈ On → (R₁ ‘x) ⊆ ℘(R₁ ‘x))
33	27, 32	syl 12	. . . . . . . . 9 ⊢ ((Lim A ∧ x ∈ A) → (R₁ ‘x) ⊆ ℘(R₁ ‘x))
34	33	exp 291	. . . . . . . 8 ⊢ (Lim A → (x ∈ A → (R₁ ‘x) ⊆ ℘(R₁ ‘x)))
35	34	r19.21aiv 1259	. . . . . . 7 ⊢ (Lim A → ∀x ∈ A (R₁ ‘x) ⊆ ℘(R₁ ‘x))
36		ss2iun 2005	. . . . . . 7 ⊢ (∀x ∈ A (R₁ ‘x) ⊆ ℘(R₁ ‘x) → ∪x ∈ A (R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
37	35, 36	syl 12	. . . . . 6 ⊢ (Lim A → ∪x ∈ A (R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
38	37	adantl 305	. . . . 5 ⊢ ((A ∈ V ∧ Lim A) → ∪x ∈ A (R₁ ‘x) ⊆ ∪x ∈ A ℘(R₁ ‘x))
39	24, 38	eqsstrd 1534	. . . 4 ⊢ ((A ∈ V ∧ Lim A) → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
40	7, 23, 39	3jaoi 633	. . 3 ⊢ ((A = ∅ ∨ ∃x ∈ On A = suc x ∨ (A ∈ V ∧ Lim A)) → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
41	1, 40	sylbi 174	. 2 ⊢ (A ∈ On → (R₁ ‘A) ⊆ ∪x ∈ A ℘(R₁ ‘x))
42		onelon 2223	. . . . . . 7 ⊢ ((A ∈ On ∧ x ∈ A) → x ∈ On)
43	42, 12	syl 12	. . . . . 6 ⊢ ((A ∈ On ∧ x ∈ A) → (R₁ ‘suc x) = ℘(R₁ ‘x))
44		r1ord3 3501	. . . . . . 7 ⊢ ((suc x ∈ On ∧ A ∈ On) → (suc x ⊆ A → (R₁ ‘suc x) ⊆ (R₁ ‘A)))
45	42, 28	sylib 173	. . . . . . . 8 ⊢ ((A ∈ On ∧ x ∈ A) → suc x ∈ On)
46		pm3.26 256	. . . . . . . 8 ⊢ ((A ∈ On ∧ x ∈ A) → A ∈ On)
47	45, 46	jca 236	. . . . . . 7 ⊢ ((A ∈ On ∧ x ∈ A) → (suc x ∈ On ∧ A ∈ On))
48		eloni 2209	. . . . . . . . 9 ⊢ (A ∈ On → Ord A)
49		ordsucss 2320	. . . . . . . . 9 ⊢ (Ord A → (x ∈ A → suc x ⊆ A))
50	48, 49	syl 12	. . . . . . . 8 ⊢ (A ∈ On → (x ∈ A → suc x ⊆ A))
51	50	imp 277	. . . . . . 7 ⊢ ((A ∈ On ∧ x ∈ A) → suc x ⊆ A)
52	44, 47, 51	sylc 62	. . . . . 6 ⊢ ((A ∈ On ∧ x ∈ A) → (R₁ ‘suc x) ⊆ (R₁ ‘A))
53	43, 52	eqsstr3d 1535	. . . . 5 ⊢ ((A ∈ On ∧ x ∈ A) → ℘(R₁ ‘x) ⊆ (R₁ ‘A))
54	53	exp 291	. . . 4 ⊢ (A ∈ On → (x ∈ A → ℘(R₁ ‘x) ⊆ (R₁ ‘A)))
55	54	r19.21aiv 1259	. . 3 ⊢ (A ∈ On → ∀x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A))
56		iunss 2017	. . 3 ⊢ (∪x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A) ↔ ∀x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A))
57	55, 56	sylibr 175	. 2 ⊢ (A ∈ On → ∪x ∈ A ℘(R₁ ‘x) ⊆ (R₁ ‘A))
58	41, 57	eqssd 1518	1 ⊢ (A ∈ On → (R₁ ‘A) = ∪x ∈ A ℘(R₁ ‘x))

Colors of variables: wff set class

Syntax hints: → wi 2 ∧ wa 196 ∨ w3o 580 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∃wrex 1202 Vcvv 1348 ⊆ wss 1487 ∅c0 1707 ℘cpw 1798 ∪ciun 1994 Ord word 2198 Oncon0 2199 Lim wlim 2200 suc csuc 2201 ‘cfv 2422 R₁cr1 3485

This theorem is referenced by: r1val3 3523

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