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 ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝒫 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )

Proof

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