r1pwss

Description: Each stage of the cumulative hierarchy of sets is closed under subsets. (Contributed by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	r1pwss	$⊢ A \in R_{1} (B) \to 𝒫 A \subseteq R_{1} (B)$

Proof

Step	Hyp	Ref	Expression
1		r1dmlim	$⊢ Lim dom R_{1}$
2		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
3	1 2	ax-mp	$⊢ Ord dom R_{1}$
4		ordsson	$⊢ Ord dom R_{1} \to dom R_{1} \subseteq On$
5	3 4	ax-mp	$⊢ dom R_{1} \subseteq On$
6		elfvdm	$⊢ A \in R_{1} (B) \to B \in dom R_{1}$
7	5 6	sselid	$⊢ A \in R_{1} (B) \to B \in On$
8		onzsl	$⊢ B \in On \leftrightarrow (B = \emptyset \lor \exists x \in On B = suc x \lor (B \in V \land Lim B))$
9	7 8	sylib	$⊢ A \in R_{1} (B) \to (B = \emptyset \lor \exists x \in On B = suc x \lor (B \in V \land Lim B))$
10		noel	$⊢ \neg A \in \emptyset$
11		fveq2	$⊢ B = \emptyset \to R_{1} (B) = R_{1} (\emptyset)$
12		r10	$⊢ R_{1} (\emptyset) = \emptyset$
13	11 12	eqtrdi	$⊢ B = \emptyset \to R_{1} (B) = \emptyset$
14	13	eleq2d	$⊢ B = \emptyset \to (A \in R_{1} (B) \leftrightarrow A \in \emptyset)$
15	14	biimpcd	$⊢ A \in R_{1} (B) \to (B = \emptyset \to A \in \emptyset)$
16	10 15	mtoi	$⊢ A \in R_{1} (B) \to \neg B = \emptyset$
17	16	pm2.21d	$⊢ A \in R_{1} (B) \to (B = \emptyset \to 𝒫 A \subseteq R_{1} (B))$
18		simpl	$⊢ (A \in R_{1} (B) \land B = suc x) \to A \in R_{1} (B)$
19		simpr	$⊢ (A \in R_{1} (B) \land B = suc x) \to B = suc x$
20	19	fveq2d	$⊢ (A \in R_{1} (B) \land B = suc x) \to R_{1} (B) = R_{1} (suc x)$
21	6	adantr	$⊢ (A \in R_{1} (B) \land B = suc x) \to B \in dom R_{1}$
22	19 21	eqeltrrd	$⊢ (A \in R_{1} (B) \land B = suc x) \to suc x \in dom R_{1}$
23		limsuc	$⊢ Lim dom R_{1} \to (x \in dom R_{1} \leftrightarrow suc x \in dom R_{1})$
24	1 23	ax-mp	$⊢ x \in dom R_{1} \leftrightarrow suc x \in dom R_{1}$
25	22 24	sylibr	$⊢ (A \in R_{1} (B) \land B = suc x) \to x \in dom R_{1}$
26		r1sucg	$⊢ x \in dom R_{1} \to R_{1} (suc x) = 𝒫 R_{1} (x)$
27	25 26	syl	$⊢ (A \in R_{1} (B) \land B = suc x) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
28	20 27	eqtrd	$⊢ (A \in R_{1} (B) \land B = suc x) \to R_{1} (B) = 𝒫 R_{1} (x)$
29	18 28	eleqtrd	$⊢ (A \in R_{1} (B) \land B = suc x) \to A \in 𝒫 R_{1} (x)$
30		elpwi	$⊢ A \in 𝒫 R_{1} (x) \to A \subseteq R_{1} (x)$
31		sspw	$⊢ A \subseteq R_{1} (x) \to 𝒫 A \subseteq 𝒫 R_{1} (x)$
32	29 30 31	3syl	$⊢ (A \in R_{1} (B) \land B = suc x) \to 𝒫 A \subseteq 𝒫 R_{1} (x)$
33	32 28	sseqtrrd	$⊢ (A \in R_{1} (B) \land B = suc x) \to 𝒫 A \subseteq R_{1} (B)$
34	33	ex	$⊢ A \in R_{1} (B) \to (B = suc x \to 𝒫 A \subseteq R_{1} (B))$
35	34	rexlimdvw	$⊢ A \in R_{1} (B) \to (\exists x \in On B = suc x \to 𝒫 A \subseteq R_{1} (B))$
36		r1tr	$⊢ Tr R_{1} (B)$
37		simpl	$⊢ (A \in R_{1} (B) \land Lim B) \to A \in R_{1} (B)$
38		r1limg	$⊢ (B \in dom R_{1} \land Lim B) \to R_{1} (B) = ⋃_{x \in B} R_{1} (x)$
39	6 38	sylan	$⊢ (A \in R_{1} (B) \land Lim B) \to R_{1} (B) = ⋃_{x \in B} R_{1} (x)$
40	37 39	eleqtrd	$⊢ (A \in R_{1} (B) \land Lim B) \to A \in ⋃_{x \in B} R_{1} (x)$
41		eliun	$⊢ A \in ⋃_{x \in B} R_{1} (x) \leftrightarrow \exists x \in B A \in R_{1} (x)$
42	40 41	sylib	$⊢ (A \in R_{1} (B) \land Lim B) \to \exists x \in B A \in R_{1} (x)$
43		simprl	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to x \in B$
44		limsuc	$⊢ Lim B \to (x \in B \leftrightarrow suc x \in B)$
45	44	ad2antlr	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to (x \in B \leftrightarrow suc x \in B)$
46	43 45	mpbid	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to suc x \in B$
47		limsuc	$⊢ Lim B \to (suc x \in B \leftrightarrow suc suc x \in B)$
48	47	ad2antlr	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to (suc x \in B \leftrightarrow suc suc x \in B)$
49	46 48	mpbid	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to suc suc x \in B$
50		r1tr	$⊢ Tr R_{1} (x)$
51		simprr	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to A \in R_{1} (x)$
52		trss	$⊢ Tr R_{1} (x) \to (A \in R_{1} (x) \to A \subseteq R_{1} (x))$
53	50 51 52	mpsyl	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to A \subseteq R_{1} (x)$
54	53 31	syl	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to 𝒫 A \subseteq 𝒫 R_{1} (x)$
55	6	ad2antrr	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to B \in dom R_{1}$
56		ordtr1	$⊢ Ord dom R_{1} \to ((x \in B \land B \in dom R_{1}) \to x \in dom R_{1})$
57	3 56	ax-mp	$⊢ (x \in B \land B \in dom R_{1}) \to x \in dom R_{1}$
58	43 55 57	syl2anc	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to x \in dom R_{1}$
59	58 26	syl	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to R_{1} (suc x) = 𝒫 R_{1} (x)$
60	54 59	sseqtrrd	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to 𝒫 A \subseteq R_{1} (suc x)$
61		fvex	$⊢ R_{1} (suc x) \in V$
62	61	elpw2	$⊢ 𝒫 A \in 𝒫 R_{1} (suc x) \leftrightarrow 𝒫 A \subseteq R_{1} (suc x)$
63	60 62	sylibr	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to 𝒫 A \in 𝒫 R_{1} (suc x)$
64	58 24	sylib	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to suc x \in dom R_{1}$
65		r1sucg	$⊢ suc x \in dom R_{1} \to R_{1} (suc suc x) = 𝒫 R_{1} (suc x)$
66	64 65	syl	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to R_{1} (suc suc x) = 𝒫 R_{1} (suc x)$
67	63 66	eleqtrrd	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to 𝒫 A \in R_{1} (suc suc x)$
68		fveq2	$⊢ y = suc suc x \to R_{1} (y) = R_{1} (suc suc x)$
69	68	eleq2d	$⊢ y = suc suc x \to (𝒫 A \in R_{1} (y) \leftrightarrow 𝒫 A \in R_{1} (suc suc x))$
70	69	rspcev	$⊢ (suc suc x \in B \land 𝒫 A \in R_{1} (suc suc x)) \to \exists y \in B 𝒫 A \in R_{1} (y)$
71	49 67 70	syl2anc	$⊢ ((A \in R_{1} (B) \land Lim B) \land (x \in B \land A \in R_{1} (x))) \to \exists y \in B 𝒫 A \in R_{1} (y)$
72	42 71	rexlimddv	$⊢ (A \in R_{1} (B) \land Lim B) \to \exists y \in B 𝒫 A \in R_{1} (y)$
73		eliun	$⊢ 𝒫 A \in ⋃_{y \in B} R_{1} (y) \leftrightarrow \exists y \in B 𝒫 A \in R_{1} (y)$
74	72 73	sylibr	$⊢ (A \in R_{1} (B) \land Lim B) \to 𝒫 A \in ⋃_{y \in B} R_{1} (y)$
75		r1limg	$⊢ (B \in dom R_{1} \land Lim B) \to R_{1} (B) = ⋃_{y \in B} R_{1} (y)$
76	6 75	sylan	$⊢ (A \in R_{1} (B) \land Lim B) \to R_{1} (B) = ⋃_{y \in B} R_{1} (y)$
77	74 76	eleqtrrd	$⊢ (A \in R_{1} (B) \land Lim B) \to 𝒫 A \in R_{1} (B)$
78		trss	$⊢ Tr R_{1} (B) \to (𝒫 A \in R_{1} (B) \to 𝒫 A \subseteq R_{1} (B))$
79	36 77 78	mpsyl	$⊢ (A \in R_{1} (B) \land Lim B) \to 𝒫 A \subseteq R_{1} (B)$
80	79	ex	$⊢ A \in R_{1} (B) \to (Lim B \to 𝒫 A \subseteq R_{1} (B))$
81	80	adantld	$⊢ A \in R_{1} (B) \to ((B \in V \land Lim B) \to 𝒫 A \subseteq R_{1} (B))$
82	17 35 81	3jaod	$⊢ A \in R_{1} (B) \to ((B = \emptyset \lor \exists x \in On B = suc x \lor (B \in V \land Lim B)) \to 𝒫 A \subseteq R_{1} (B))$
83	9 82	mpd	$⊢ A \in R_{1} (B) \to 𝒫 A \subseteq R_{1} (B)$

Metamath Proof Explorer

Theorem r1pwss

Proof