Metamath Proof Explorer

Theorem eldifsucnn

Description: Condition for membership in the difference of _om and a nonzero finite ordinal. (Contributed by Scott Fenton, 24-Oct-2024)

Ref Expression
Assertion eldifsucnn 
|- ( A e. _om -> ( B e. ( _om \ suc A ) <-> E. x e. ( _om \ A ) B = suc x ) )

Proof

Step Hyp Ref Expression
1 peano2 
 |-  ( A e. _om -> suc A e. _om )
2 nnawordex 
 |-  ( ( suc A e. _om /\ B e. _om ) -> ( suc A C_ B <-> E. y e. _om ( suc A +o y ) = B ) )
3 1 2 sylan 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc A C_ B <-> E. y e. _om ( suc A +o y ) = B ) )
4 nnacl 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A +o y ) e. _om )
5 nnaword1 
 |-  ( ( A e. _om /\ y e. _om ) -> A C_ ( A +o y ) )
6 nnasuc 
 |-  ( ( y e. _om /\ A e. _om ) -> ( y +o suc A ) = suc ( y +o A ) )
7 6 ancoms 
 |-  ( ( A e. _om /\ y e. _om ) -> ( y +o suc A ) = suc ( y +o A ) )
8 nnacom 
 |-  ( ( suc A e. _om /\ y e. _om ) -> ( suc A +o y ) = ( y +o suc A ) )
9 1 8 sylan 
 |-  ( ( A e. _om /\ y e. _om ) -> ( suc A +o y ) = ( y +o suc A ) )
10 nnacom 
 |-  ( ( A e. _om /\ y e. _om ) -> ( A +o y ) = ( y +o A ) )
11 suceq 
 |-  ( ( A +o y ) = ( y +o A ) -> suc ( A +o y ) = suc ( y +o A ) )
12 10 11 syl 
 |-  ( ( A e. _om /\ y e. _om ) -> suc ( A +o y ) = suc ( y +o A ) )
13 7 9 12 3eqtr4d 
 |-  ( ( A e. _om /\ y e. _om ) -> ( suc A +o y ) = suc ( A +o y ) )
14 sseq2 
 |-  ( x = ( A +o y ) -> ( A C_ x <-> A C_ ( A +o y ) ) )
15 suceq 
 |-  ( x = ( A +o y ) -> suc x = suc ( A +o y ) )
16 15 eqeq2d 
 |-  ( x = ( A +o y ) -> ( ( suc A +o y ) = suc x <-> ( suc A +o y ) = suc ( A +o y ) ) )
17 14 16 anbi12d 
 |-  ( x = ( A +o y ) -> ( ( A C_ x /\ ( suc A +o y ) = suc x ) <-> ( A C_ ( A +o y ) /\ ( suc A +o y ) = suc ( A +o y ) ) ) )
18 17 rspcev 
 |-  ( ( ( A +o y ) e. _om /\ ( A C_ ( A +o y ) /\ ( suc A +o y ) = suc ( A +o y ) ) ) -> E. x e. _om ( A C_ x /\ ( suc A +o y ) = suc x ) )
19 4 5 13 18 syl12anc 
 |-  ( ( A e. _om /\ y e. _om ) -> E. x e. _om ( A C_ x /\ ( suc A +o y ) = suc x ) )
20 eqeq1 
 |-  ( ( suc A +o y ) = B -> ( ( suc A +o y ) = suc x <-> B = suc x ) )
21 20 anbi2d 
 |-  ( ( suc A +o y ) = B -> ( ( A C_ x /\ ( suc A +o y ) = suc x ) <-> ( A C_ x /\ B = suc x ) ) )
22 21 rexbidv 
 |-  ( ( suc A +o y ) = B -> ( E. x e. _om ( A C_ x /\ ( suc A +o y ) = suc x ) <-> E. x e. _om ( A C_ x /\ B = suc x ) ) )
23 19 22 syl5ibcom 
 |-  ( ( A e. _om /\ y e. _om ) -> ( ( suc A +o y ) = B -> E. x e. _om ( A C_ x /\ B = suc x ) ) )
24 23 rexlimdva 
 |-  ( A e. _om -> ( E. y e. _om ( suc A +o y ) = B -> E. x e. _om ( A C_ x /\ B = suc x ) ) )
25 24 adantr 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. y e. _om ( suc A +o y ) = B -> E. x e. _om ( A C_ x /\ B = suc x ) ) )
26 3 25 sylbid 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc A C_ B -> E. x e. _om ( A C_ x /\ B = suc x ) ) )
27 26 expimpd 
 |-  ( A e. _om -> ( ( B e. _om /\ suc A C_ B ) -> E. x e. _om ( A C_ x /\ B = suc x ) ) )
28 peano2 
 |-  ( x e. _om -> suc x e. _om )
29 28 ad2antlr 
 |-  ( ( ( A e. _om /\ x e. _om ) /\ A C_ x ) -> suc x e. _om )
30 nnord 
 |-  ( A e. _om -> Ord A )
31 nnord 
 |-  ( x e. _om -> Ord x )
32 ordsucsssuc 
 |-  ( ( Ord A /\ Ord x ) -> ( A C_ x <-> suc A C_ suc x ) )
33 30 31 32 syl2an 
 |-  ( ( A e. _om /\ x e. _om ) -> ( A C_ x <-> suc A C_ suc x ) )
34 33 biimpa 
 |-  ( ( ( A e. _om /\ x e. _om ) /\ A C_ x ) -> suc A C_ suc x )
35 29 34 jca 
 |-  ( ( ( A e. _om /\ x e. _om ) /\ A C_ x ) -> ( suc x e. _om /\ suc A C_ suc x ) )
36 eleq1 
 |-  ( B = suc x -> ( B e. _om <-> suc x e. _om ) )
37 sseq2 
 |-  ( B = suc x -> ( suc A C_ B <-> suc A C_ suc x ) )
38 36 37 anbi12d 
 |-  ( B = suc x -> ( ( B e. _om /\ suc A C_ B ) <-> ( suc x e. _om /\ suc A C_ suc x ) ) )
39 35 38 syl5ibrcom 
 |-  ( ( ( A e. _om /\ x e. _om ) /\ A C_ x ) -> ( B = suc x -> ( B e. _om /\ suc A C_ B ) ) )
40 39 expimpd 
 |-  ( ( A e. _om /\ x e. _om ) -> ( ( A C_ x /\ B = suc x ) -> ( B e. _om /\ suc A C_ B ) ) )
41 40 rexlimdva 
 |-  ( A e. _om -> ( E. x e. _om ( A C_ x /\ B = suc x ) -> ( B e. _om /\ suc A C_ B ) ) )
42 27 41 impbid 
 |-  ( A e. _om -> ( ( B e. _om /\ suc A C_ B ) <-> E. x e. _om ( A C_ x /\ B = suc x ) ) )
43 eldif 
 |-  ( B e. ( _om \ suc A ) <-> ( B e. _om /\ -. B e. suc A ) )
44 nnord 
 |-  ( suc A e. _om -> Ord suc A )
45 1 44 syl 
 |-  ( A e. _om -> Ord suc A )
46 nnord 
 |-  ( B e. _om -> Ord B )
47 ordtri1 
 |-  ( ( Ord suc A /\ Ord B ) -> ( suc A C_ B <-> -. B e. suc A ) )
48 45 46 47 syl2an 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc A C_ B <-> -. B e. suc A ) )
49 48 pm5.32da 
 |-  ( A e. _om -> ( ( B e. _om /\ suc A C_ B ) <-> ( B e. _om /\ -. B e. suc A ) ) )
50 43 49 bitr4id 
 |-  ( A e. _om -> ( B e. ( _om \ suc A ) <-> ( B e. _om /\ suc A C_ B ) ) )
51 eldif 
 |-  ( x e. ( _om \ A ) <-> ( x e. _om /\ -. x e. A ) )
52 51 anbi1i 
 |-  ( ( x e. ( _om \ A ) /\ B = suc x ) <-> ( ( x e. _om /\ -. x e. A ) /\ B = suc x ) )
53 anass 
 |-  ( ( ( x e. _om /\ -. x e. A ) /\ B = suc x ) <-> ( x e. _om /\ ( -. x e. A /\ B = suc x ) ) )
54 52 53 bitri 
 |-  ( ( x e. ( _om \ A ) /\ B = suc x ) <-> ( x e. _om /\ ( -. x e. A /\ B = suc x ) ) )
55 54 rexbii2 
 |-  ( E. x e. ( _om \ A ) B = suc x <-> E. x e. _om ( -. x e. A /\ B = suc x ) )
56 ordtri1 
 |-  ( ( Ord A /\ Ord x ) -> ( A C_ x <-> -. x e. A ) )
57 30 31 56 syl2an 
 |-  ( ( A e. _om /\ x e. _om ) -> ( A C_ x <-> -. x e. A ) )
58 57 anbi1d 
 |-  ( ( A e. _om /\ x e. _om ) -> ( ( A C_ x /\ B = suc x ) <-> ( -. x e. A /\ B = suc x ) ) )
59 58 rexbidva 
 |-  ( A e. _om -> ( E. x e. _om ( A C_ x /\ B = suc x ) <-> E. x e. _om ( -. x e. A /\ B = suc x ) ) )
60 55 59 bitr4id 
 |-  ( A e. _om -> ( E. x e. ( _om \ A ) B = suc x <-> E. x e. _om ( A C_ x /\ B = suc x ) ) )
61 42 50 60 3bitr4d 
 |-  ( A e. _om -> ( B e. ( _om \ suc A ) <-> E. x e. ( _om \ A ) B = suc x ) )