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		r1dmlim	$⊢ Lim dom R_{1}$
11		limsuc	$⊢ Lim dom R_{1} \to (rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1})$
12	10 11	ax-mp	$⊢ rank (A) \in dom R_{1} \leftrightarrow suc rank (A) \in dom R_{1}$
13	3 12	mpbi	$⊢ suc rank (A) \in dom R_{1}$
14		r1sucg	$⊢ suc rank (A) \in dom R_{1} \to R_{1} (suc suc rank (A)) = 𝒫 R_{1} (suc rank (A))$
15	13 14	ax-mp	$⊢ R_{1} (suc suc rank (A)) = 𝒫 R_{1} (suc rank (A))$
16	9 15	eleqtrrdi	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \in R_{1} (suc suc rank (A))$
17		r1elwf	$⊢ 𝒫 A \in R_{1} (suc suc rank (A)) \to 𝒫 A \in ⋃ R_{1} [On]$
18	16 17	syl	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \in ⋃ R_{1} [On]$
19		r1elssi	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to 𝒫 A \subseteq ⋃ R_{1} [On]$
20		pwexr	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to A \in V$
21		pwidg	$⊢ A \in V \to A \in 𝒫 A$
22	20 21	syl	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to A \in 𝒫 A$
23	19 22	sseldd	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to A \in ⋃ R_{1} [On]$
24	18 23	impbii	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow 𝒫 A \in ⋃ R_{1} [On]$

Metamath Proof Explorer

Theorem pwwf

Proof