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