r1pwss

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

Metamath Proof Explorer

Theorem r1pwss

Proof