pwwf

Description: A power set is well-founded iff the base set is. (Contributed by Mario Carneiro, 8-Jun-2013) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	pwwf	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow 𝒫 A \in ⋃ R_{1} [On]$

Proof

Step	Hyp	Ref	Expression
1		r1rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq R_{1} (rank (A))$
2	1	sspwd	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \subseteq 𝒫 R_{1} (rank (A))$
3		rankdmr1	$⊢ rank (A) \in dom R_{1}$
4		r1sucg	$⊢ rank (A) \in dom R_{1} \to R_{1} (suc rank (A)) = 𝒫 R_{1} (rank (A))$
5	3 4	ax-mp	$⊢ R_{1} (suc rank (A)) = 𝒫 R_{1} (rank (A))$
6	2 5	sseqtrrdi	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \subseteq R_{1} (suc rank (A))$
7		fvex	$⊢ R_{1} (suc rank (A)) \in V$
8	7	elpw2	$⊢ 𝒫 A \in 𝒫 R_{1} (suc rank (A)) \leftrightarrow 𝒫 A \subseteq R_{1} (suc rank (A))$
9	6 8	sylibr	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \in 𝒫 R_{1} (suc rank (A))$
10		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
11	10	simpri	$⊢ Lim dom R_{1}$
12		limsuc	$⊢ Lim dom R_{1} \to (rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1})$
13	11 12	ax-mp	$⊢ rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1}$
14	3 13	mpbi	$⊢ suc rank (A) \in dom R_{1}$
15		r1sucg	$⊢ suc rank (A) \in dom R_{1} \to R_{1} (suc suc rank (A)) = 𝒫 R_{1} (suc rank (A))$
16	14 15	ax-mp	$⊢ R_{1} (suc suc rank (A)) = 𝒫 R_{1} (suc rank (A))$
17	9 16	eleqtrrdi	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \in R_{1} (suc suc rank (A))$
18		r1elwf	$⊢ 𝒫 A \in R_{1} (suc suc rank (A)) \to 𝒫 A \in ⋃ R_{1} [On]$
19	17 18	syl	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \in ⋃ R_{1} [On]$
20		r1elssi	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to 𝒫 A \subseteq ⋃ R_{1} [On]$
21		pwexr	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to A \in V$
22		pwidg	$⊢ A \in V \to A \in 𝒫 A$
23	21 22	syl	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to A \in 𝒫 A$
24	20 23	sseldd	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to A \in ⋃ R_{1} [On]$
25	19 24	impbii	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow 𝒫 A \in ⋃ R_{1} [On]$

Metamath Proof Explorer

Theorem pwwf

Proof