Metamath Proof Explorer

Theorem r1pwALT

Description: Alternate shorter proof of r1pw based on the additional axioms ax-reg and ax-inf2 . (Contributed by Raph Levien, 29-May-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion r1pwALT ⊢ B ∈ On → A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ x = A → x ∈ R1 ⁡ B ↔ A ∈ R1 ⁡ B
2 pweq ⊢ x = A → 𝒫 x = 𝒫 A
3 2 eleq1d ⊢ x = A → 𝒫 x ∈ R1 ⁡ suc ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B
4 1 3 bibi12d ⊢ x = A → x ∈ R1 ⁡ B ↔ 𝒫 x ∈ R1 ⁡ suc ⁡ B ↔ A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B
5 4 imbi2d ⊢ x = A → B ∈ On → x ∈ R1 ⁡ B ↔ 𝒫 x ∈ R1 ⁡ suc ⁡ B ↔ B ∈ On → A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B
6 vex ⊢ x ∈ V
7 6 rankr1a ⊢ B ∈ On → x ∈ R1 ⁡ B ↔ rank ⁡ x ∈ B
8 eloni ⊢ B ∈ On → Ord ⁡ B
9 ordsucelsuc ⊢ Ord ⁡ B → rank ⁡ x ∈ B ↔ suc ⁡ rank ⁡ x ∈ suc ⁡ B
10 8 9 syl ⊢ B ∈ On → rank ⁡ x ∈ B ↔ suc ⁡ rank ⁡ x ∈ suc ⁡ B
11 7 10 bitrd ⊢ B ∈ On → x ∈ R1 ⁡ B ↔ suc ⁡ rank ⁡ x ∈ suc ⁡ B
12 6 rankpw ⊢ rank ⁡ 𝒫 x = suc ⁡ rank ⁡ x
13 12 eleq1i ⊢ rank ⁡ 𝒫 x ∈ suc ⁡ B ↔ suc ⁡ rank ⁡ x ∈ suc ⁡ B
14 11 13 bitr4di ⊢ B ∈ On → x ∈ R1 ⁡ B ↔ rank ⁡ 𝒫 x ∈ suc ⁡ B
15 suceloni ⊢ B ∈ On → suc ⁡ B ∈ On
16 6 pwex ⊢ 𝒫 x ∈ V
17 16 rankr1a ⊢ suc ⁡ B ∈ On → 𝒫 x ∈ R1 ⁡ suc ⁡ B ↔ rank ⁡ 𝒫 x ∈ suc ⁡ B
18 15 17 syl ⊢ B ∈ On → 𝒫 x ∈ R1 ⁡ suc ⁡ B ↔ rank ⁡ 𝒫 x ∈ suc ⁡ B
19 14 18 bitr4d ⊢ B ∈ On → x ∈ R1 ⁡ B ↔ 𝒫 x ∈ R1 ⁡ suc ⁡ B
20 5 19 vtoclg ⊢ A ∈ V → B ∈ On → A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B
21 elex ⊢ A ∈ R1 ⁡ B → A ∈ V
22 elex ⊢ 𝒫 A ∈ R1 ⁡ suc ⁡ B → 𝒫 A ∈ V
23 pwexb ⊢ A ∈ V ↔ 𝒫 A ∈ V
24 22 23 sylibr ⊢ 𝒫 A ∈ R1 ⁡ suc ⁡ B → A ∈ V
25 21 24 pm5.21ni ⊢ ¬ A ∈ V → A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B
26 25 a1d ⊢ ¬ A ∈ V → B ∈ On → A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B
27 20 26 pm2.61i ⊢ B ∈ On → A ∈ R1 ⁡ B ↔ 𝒫 A ∈ R1 ⁡ suc ⁡ B