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 e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = A -> ( x e. ( R1 ` B ) <-> A e. ( R1 ` B ) ) )
2 pweq 
 |-  ( x = A -> ~P x = ~P A )
3 2 eleq1d 
 |-  ( x = A -> ( ~P x e. ( R1 ` suc B ) <-> ~P A e. ( R1 ` suc B ) ) )
4 1 3 bibi12d 
 |-  ( x = A -> ( ( x e. ( R1 ` B ) <-> ~P x e. ( R1 ` suc B ) ) <-> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) )
5 4 imbi2d 
 |-  ( x = A -> ( ( B e. On -> ( x e. ( R1 ` B ) <-> ~P x e. ( R1 ` suc B ) ) ) <-> ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) ) )
6 vex 
 |-  x e. _V
7 6 rankr1a 
 |-  ( B e. On -> ( x e. ( R1 ` B ) <-> ( rank ` x ) e. B ) )
8 eloni 
 |-  ( B e. On -> Ord B )
9 ordsucelsuc 
 |-  ( Ord B -> ( ( rank ` x ) e. B <-> suc ( rank ` x ) e. suc B ) )
10 8 9 syl 
 |-  ( B e. On -> ( ( rank ` x ) e. B <-> suc ( rank ` x ) e. suc B ) )
11 7 10 bitrd 
 |-  ( B e. On -> ( x e. ( R1 ` B ) <-> suc ( rank ` x ) e. suc B ) )
12 6 rankpw 
 |-  ( rank ` ~P x ) = suc ( rank ` x )
13 12 eleq1i 
 |-  ( ( rank ` ~P x ) e. suc B <-> suc ( rank ` x ) e. suc B )
14 11 13 bitr4di 
 |-  ( B e. On -> ( x e. ( R1 ` B ) <-> ( rank ` ~P x ) e. suc B ) )
15 suceloni 
 |-  ( B e. On -> suc B e. On )
16 6 pwex 
 |-  ~P x e. _V
17 16 rankr1a 
 |-  ( suc B e. On -> ( ~P x e. ( R1 ` suc B ) <-> ( rank ` ~P x ) e. suc B ) )
18 15 17 syl 
 |-  ( B e. On -> ( ~P x e. ( R1 ` suc B ) <-> ( rank ` ~P x ) e. suc B ) )
19 14 18 bitr4d 
 |-  ( B e. On -> ( x e. ( R1 ` B ) <-> ~P x e. ( R1 ` suc B ) ) )
20 5 19 vtoclg 
 |-  ( A e. _V -> ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) )
21 elex 
 |-  ( A e. ( R1 ` B ) -> A e. _V )
22 elex 
 |-  ( ~P A e. ( R1 ` suc B ) -> ~P A e. _V )
23 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
24 22 23 sylibr 
 |-  ( ~P A e. ( R1 ` suc B ) -> A e. _V )
25 21 24 pm5.21ni 
 |-  ( -. A e. _V -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )
26 25 a1d 
 |-  ( -. A e. _V -> ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) ) )
27 20 26 pm2.61i 
 |-  ( B e. On -> ( A e. ( R1 ` B ) <-> ~P A e. ( R1 ` suc B ) ) )