r1pw

Description: A stronger property of R1 than rankpw . The latter merely proves that R1 of the successor is a power set, but here we prove that if A is in the cumulative hierarchy, then ~P A is in the cumulative hierarchy of the successor. (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		suceloni	$⊢ B \in On \to suc B \in On$
11		r1fnon	$⊢ R_{1} Fn On$
12		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
13	11 12	ax-mp	$⊢ dom R_{1} = On$
14	10 13	eleqtrrdi	$⊢ B \in On \to suc B \in dom R_{1}$
15		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)$
16	9 14 15	syl2an	$⊢ (A \in ⋃ R_{1} [On] \land B \in On) \to (𝒫 A \in R_{1} (suc B) \leftrightarrow rank (𝒫 A) \in suc B)$
17	13	eleq2i	$⊢ B \in dom R_{1} \leftrightarrow B \in On$
18		rankr1ag	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$
19	17 18	sylan2br	$⊢ (A \in ⋃ R_{1} [On] \land B \in On) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$
20	7 16 19	3bitr4rd	$⊢ (A \in ⋃ R_{1} [On] \land B \in On) \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B))$
21	20	ex	$⊢ A \in ⋃ R_{1} [On] \to (B \in On \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B)))$
22		r1elwf	$⊢ A \in R_{1} (B) \to A \in ⋃ R_{1} [On]$
23		r1elwf	$⊢ 𝒫 A \in R_{1} (suc B) \to 𝒫 A \in ⋃ R_{1} [On]$
24		r1elssi	$⊢ 𝒫 A \in ⋃ R_{1} [On] \to 𝒫 A \subseteq ⋃ R_{1} [On]$
25	23 24	syl	$⊢ 𝒫 A \in R_{1} (suc B) \to 𝒫 A \subseteq ⋃ R_{1} [On]$
26		ssid	$⊢ A \subseteq A$
27		pwexr	$⊢ 𝒫 A \in R_{1} (suc B) \to A \in V$
28		elpwg	$⊢ A \in V \to (A \in 𝒫 A \leftrightarrow A \subseteq A)$
29	27 28	syl	$⊢ 𝒫 A \in R_{1} (suc B) \to (A \in 𝒫 A \leftrightarrow A \subseteq A)$
30	26 29	mpbiri	$⊢ 𝒫 A \in R_{1} (suc B) \to A \in 𝒫 A$
31	25 30	sseldd	$⊢ 𝒫 A \in R_{1} (suc B) \to A \in ⋃ R_{1} [On]$
32	22 31	pm5.21ni	$⊢ \neg A \in ⋃ R_{1} [On] \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B))$
33	32	a1d	$⊢ \neg A \in ⋃ R_{1} [On] \to (B \in On \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B)))$
34	21 33	pm2.61i	$⊢ B \in On \to (A \in R_{1} (B) \leftrightarrow 𝒫 A \in R_{1} (suc B))$

Metamath Proof Explorer

Theorem r1pw

Proof