Metamath Proof Explorer

Theorem peano5OLD

Description: Obsolete version of peano5 as of 3-Oct-2024. (Contributed by NM, 18-Feb-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion peano5OLD ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ω ⊆ 𝐴 )

Proof

Step Hyp Ref Expression
1 eldifn ⊢ ( 𝑦 ∈ ( ω ∖ 𝐴 ) → ¬ 𝑦 ∈ 𝐴 )
2 1 adantl ⊢ ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑦 ∈ ( ω ∖ 𝐴 ) ) → ¬ 𝑦 ∈ 𝐴 )
3 eldifi ⊢ ( 𝑦 ∈ ( ω ∖ 𝐴 ) → 𝑦 ∈ ω )
4 elndif ⊢ ( ∅ ∈ 𝐴 → ¬ ∅ ∈ ( ω ∖ 𝐴 ) )
5 eleq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ ( ω ∖ 𝐴 ) ↔ ∅ ∈ ( ω ∖ 𝐴 ) ) )
6 5 biimpcd ⊢ ( 𝑦 ∈ ( ω ∖ 𝐴 ) → ( 𝑦 = ∅ → ∅ ∈ ( ω ∖ 𝐴 ) ) )
7 6 necon3bd ⊢ ( 𝑦 ∈ ( ω ∖ 𝐴 ) → ( ¬ ∅ ∈ ( ω ∖ 𝐴 ) → 𝑦 ≠ ∅ ) )
8 4 7 mpan9 ⊢ ( ( ∅ ∈ 𝐴 ∧ 𝑦 ∈ ( ω ∖ 𝐴 ) ) → 𝑦 ≠ ∅ )
9 nnsuc ⊢ ( ( 𝑦 ∈ ω ∧ 𝑦 ≠ ∅ ) → ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 )
10 3 8 9 syl2an2 ⊢ ( ( ∅ ∈ 𝐴 ∧ 𝑦 ∈ ( ω ∖ 𝐴 ) ) → ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 )
11 10 ad4ant13 ⊢ ( ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑦 ∈ ( ω ∖ 𝐴 ) ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) → ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 )
12 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 )
13 nfv ⊢ Ⅎ 𝑥 ( 𝑦 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ )
14 12 13 nfan ⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) )
15 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
16 rsp ⊢ ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ω → ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) )
17 vex ⊢ 𝑥 ∈ V
18 17 sucid ⊢ 𝑥 ∈ suc 𝑥
19 eleq2 ⊢ ( 𝑦 = suc 𝑥 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ suc 𝑥 ) )
20 18 19 mpbiri ⊢ ( 𝑦 = suc 𝑥 → 𝑥 ∈ 𝑦 )
21 eleq1 ⊢ ( 𝑦 = suc 𝑥 → ( 𝑦 ∈ ω ↔ suc 𝑥 ∈ ω ) )
22 peano2b ⊢ ( 𝑥 ∈ ω ↔ suc 𝑥 ∈ ω )
23 21 22 bitr4di ⊢ ( 𝑦 = suc 𝑥 → ( 𝑦 ∈ ω ↔ 𝑥 ∈ ω ) )
24 minel ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) → ¬ 𝑥 ∈ ( ω ∖ 𝐴 ) )
25 neldif ⊢ ( ( 𝑥 ∈ ω ∧ ¬ 𝑥 ∈ ( ω ∖ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
26 24 25 sylan2 ⊢ ( ( 𝑥 ∈ ω ∧ ( 𝑥 ∈ 𝑦 ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) ) → 𝑥 ∈ 𝐴 )
27 26 exp32 ⊢ ( 𝑥 ∈ ω → ( 𝑥 ∈ 𝑦 → ( ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ → 𝑥 ∈ 𝐴 ) ) )
28 23 27 syl6bi ⊢ ( 𝑦 = suc 𝑥 → ( 𝑦 ∈ ω → ( 𝑥 ∈ 𝑦 → ( ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ → 𝑥 ∈ 𝐴 ) ) ) )
29 20 28 mpid ⊢ ( 𝑦 = suc 𝑥 → ( 𝑦 ∈ ω → ( ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ → 𝑥 ∈ 𝐴 ) ) )
30 3 29 syl5 ⊢ ( 𝑦 = suc 𝑥 → ( 𝑦 ∈ ( ω ∖ 𝐴 ) → ( ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ → 𝑥 ∈ 𝐴 ) ) )
31 30 impd ⊢ ( 𝑦 = suc 𝑥 → ( ( 𝑦 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) → 𝑥 ∈ 𝐴 ) )
32 eleq1a ⊢ ( suc 𝑥 ∈ 𝐴 → ( 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴 ) )
33 32 com12 ⊢ ( 𝑦 = suc 𝑥 → ( suc 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴 ) )
34 31 33 imim12d ⊢ ( 𝑦 = suc 𝑥 → ( ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( ( 𝑦 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ 𝐴 ) ) )
35 34 com13 ⊢ ( ( 𝑦 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) → ( ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴 ) ) )
36 16 35 sylan9 ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) ) → ( 𝑥 ∈ ω → ( 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴 ) ) )
37 14 15 36 rexlimd ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ∧ ( 𝑦 ∈ ( ω ∖ 𝐴 ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) ) → ( ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴 ) )
38 37 exp32 ⊢ ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( ω ∖ 𝐴 ) → ( ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ → ( ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴 ) ) ) )
39 38 a1i ⊢ ( ∅ ∈ 𝐴 → ( ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( ω ∖ 𝐴 ) → ( ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ → ( ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴 ) ) ) ) )
40 39 imp41 ⊢ ( ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑦 ∈ ( ω ∖ 𝐴 ) ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) → ( ∃ 𝑥 ∈ ω 𝑦 = suc 𝑥 → 𝑦 ∈ 𝐴 ) )
41 11 40 mpd ⊢ ( ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑦 ∈ ( ω ∖ 𝐴 ) ) ∧ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ 𝐴 )
42 2 41 mtand ⊢ ( ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) ∧ 𝑦 ∈ ( ω ∖ 𝐴 ) ) → ¬ ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ )
43 42 nrexdv ⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ¬ ∃ 𝑦 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ )
44 ordom ⊢ Ord ω
45 difss ⊢ ( ω ∖ 𝐴 ) ⊆ ω
46 tz7.5 ⊢ ( ( Ord ω ∧ ( ω ∖ 𝐴 ) ⊆ ω ∧ ( ω ∖ 𝐴 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ )
47 44 45 46 mp3an12 ⊢ ( ( ω ∖ 𝐴 ) ≠ ∅ → ∃ 𝑦 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ )
48 47 necon1bi ⊢ ( ¬ ∃ 𝑦 ∈ ( ω ∖ 𝐴 ) ( ( ω ∖ 𝐴 ) ∩ 𝑦 ) = ∅ → ( ω ∖ 𝐴 ) = ∅ )
49 43 48 syl ⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ( ω ∖ 𝐴 ) = ∅ )
50 ssdif0 ⊢ ( ω ⊆ 𝐴 ↔ ( ω ∖ 𝐴 ) = ∅ )
51 49 50 sylibr ⊢ ( ( ∅ ∈ 𝐴 ∧ ∀ 𝑥 ∈ ω ( 𝑥 ∈ 𝐴 → suc 𝑥 ∈ 𝐴 ) ) → ω ⊆ 𝐴 )