This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ω → ( 𝐵 ∈ ( ω ∖ suc 𝐴 ) ↔ ∃ 𝑥 ∈ ( ω ∖ 𝐴 ) 𝐵 = suc 𝑥 ) )

Proof

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