r1pw

Description: A set is in a given stage of the cumulative hierarchy of sets if and only if its powerset is in the successor stage. (Contributed by Raph Levien, 29-May-2004) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	r1pw	$⊢ B \in On \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B))$

Proof

Step	Hyp	Ref	Expression
1		rankpwi	$⊢ A \in ⋃ R_{1} [On] \to rank (𝒫 A) = suc rank (A)$
2	1	eleq1d	$⊢ A \in ⋃ R_{1} [On] \to (rank (𝒫 A) \in suc B \leftrightarrow suc rank (A) \in suc B)$
3		eloni	$⊢ B \in On \to Ord B$
4		ordsucelsuc	$⊢ Ord B \to (rank (A) \in B \leftrightarrow suc rank (A) \in suc B)$
5	3 4	syl	$⊢ B \in On \to (rank (A) \in B \leftrightarrow suc rank (A) \in suc B)$
6	5	bicomd	$⊢ B \in On \to (suc rank (A) \in suc B \leftrightarrow rank (A) \in B)$
7	2 6	sylan9bb	$⊢ (A \in ⋃ R_{1} [On] \land B \in On) \to (rank (𝒫 A) \in suc B \leftrightarrow rank (A) \in B)$
8		pwwf	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow 𝒫 A \in ⋃ R_{1} [On]$
9	8	biimpi	$⊢ A \in ⋃ R_{1} [On] \to 𝒫 A \in ⋃ R_{1} [On]$
10		onsuc	$⊢ B \in On \to suc B \in On$
11		r1fnon	$⊢ R_{1} Fn On$
12	11	fndmi	$⊢ dom R_{1} = On$
13	10 12	eleqtrrdi	$⊢ B \in On \to suc B \in dom R_{1}$
14		rankr1ag	$⊢ (𝒫 A \in ⋃ R_{1} [On] \land suc B \in dom R_{1}) \to (𝒫 A \in R_{1} (suc B) \leftrightarrow rank (𝒫 A) \in suc B)$
15	9 13 14	syl2an	$⊢ (A \in ⋃ R_{1} [On] \land B \in On) \to (𝒫 A \in R_{1} (suc B) \leftrightarrow rank (𝒫 A) \in suc B)$
16	12	eleq2i	$⊢ B \in dom R_{1} \leftrightarrow B \in On$
17		rankr1ag	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$
18	16 17	sylan2br	$⊢ (A \in ⋃ R_{1} [On] \land B \in On) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$
19	7 15 18	3bitr4rd	$⊢ (A \in ⋃ R_{1} [On] \land B \in On) \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B))$
20	19	ex	$⊢ A \in ⋃ R_{1} [On] \to (B \in On \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B)))$
21		r1elwf	$⊢ A \in R_{1} (B) \to A \in ⋃ R_{1} [On]$
22		r1elwf	$⊢ 𝒫 A \in R_{1} (suc B) \to 𝒫 A \in ⋃ R_{1} [On]$
23		r1elssi	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to 𝒫 A \subseteq ⋃ R_{1} [On]$
24	22 23	syl	$⊢ 𝒫 A \in R_{1} (suc B) \to 𝒫 A \subseteq ⋃ R_{1} [On]$
25		ssid	$⊢ A \subseteq A$
26		pwexr	$⊢ 𝒫 A \in R_{1} (suc B) \to A \in V$
27		elpwg	$⊢ A \in V \to (A \in 𝒫 A \leftrightarrow A \subseteq A)$
28	26 27	syl	$⊢ 𝒫 A \in R_{1} (suc B) \to (A \in 𝒫 A \leftrightarrow A \subseteq A)$
29	25 28	mpbiri	$⊢ 𝒫 A \in R_{1} (suc B) \to A \in 𝒫 A$
30	24 29	sseldd	$⊢ 𝒫 A \in R_{1} (suc B) \to A \in ⋃ R_{1} [On]$
31	21 30	pm5.21ni	$⊢ \neg A \in ⋃ R_{1} [On] \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B))$
32	31	a1d	$⊢ \neg A \in ⋃ R_{1} [On] \to (B \in On \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B)))$
33	20 32	pm2.61i	$⊢ B \in On \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B))$

Metamath Proof Explorer

Theorem r1pw

Proof