Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ctinf GIF version

Theorem ctinf 11977
 Description: A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.)
Assertion
Ref Expression
ctinf (𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴))
Distinct variable group:   𝐴,𝑓,𝑦,𝑥

Proof of Theorem ctinf
Dummy variables 𝑎 𝑏 𝑛 𝑘 𝑢 𝑔 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ctinfom 11975 . . . 4 (𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
21simplbi 272 . . 3 (𝐴 ≈ ℕ → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
31simprbi 273 . . . 4 (𝐴 ≈ ℕ → ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
4 simpl 108 . . . . . 6 ((𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → 𝑓:ω–onto𝐴)
54a1i 9 . . . . 5 (𝐴 ≈ ℕ → ((𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → 𝑓:ω–onto𝐴))
65eximdv 1853 . . . 4 (𝐴 ≈ ℕ → (∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)) → ∃𝑓 𝑓:ω–onto𝐴))
73, 6mpd 13 . . 3 (𝐴 ≈ ℕ → ∃𝑓 𝑓:ω–onto𝐴)
8 nnenom 10237 . . . . . 6 ℕ ≈ ω
9 entr 6685 . . . . . 6 ((𝐴 ≈ ℕ ∧ ℕ ≈ ω) → 𝐴 ≈ ω)
108, 9mpan2 422 . . . . 5 (𝐴 ≈ ℕ → 𝐴 ≈ ω)
1110ensymd 6684 . . . 4 (𝐴 ≈ ℕ → ω ≈ 𝐴)
12 endom 6664 . . . 4 (ω ≈ 𝐴 → ω ≼ 𝐴)
1311, 12syl 14 . . 3 (𝐴 ≈ ℕ → ω ≼ 𝐴)
142, 7, 133jca 1162 . 2 (𝐴 ≈ ℕ → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴))
15 simp1 982 . . 3 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
16 3simpb 980 . . . 4 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴))
17 simp2 983 . . . 4 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → ∃𝑓 𝑓:ω–onto𝐴)
18 simp2 983 . . . . . . . 8 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → 𝑓:ω–onto𝐴)
19 simpl1 985 . . . . . . . . . . . 12 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
20 equequ1 1689 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (𝑥 = 𝑦𝑢 = 𝑦))
2120dcbid 824 . . . . . . . . . . . . . 14 (𝑥 = 𝑢 → (DECID 𝑥 = 𝑦DECID 𝑢 = 𝑦))
2221ralbidv 2438 . . . . . . . . . . . . 13 (𝑥 = 𝑢 → (∀𝑦𝐴 DECID 𝑥 = 𝑦 ↔ ∀𝑦𝐴 DECID 𝑢 = 𝑦))
2322cbvralv 2657 . . . . . . . . . . . 12 (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ↔ ∀𝑢𝐴𝑦𝐴 DECID 𝑢 = 𝑦)
2419, 23sylib 121 . . . . . . . . . . 11 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∀𝑢𝐴𝑦𝐴 DECID 𝑢 = 𝑦)
25 simpl3 987 . . . . . . . . . . 11 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ω ≼ 𝐴)
26 fof 5352 . . . . . . . . . . . . . 14 (𝑓:ω–onto𝐴𝑓:ω⟶𝐴)
27 imassrn 4899 . . . . . . . . . . . . . . 15 (𝑓𝑛) ⊆ ran 𝑓
28 frn 5288 . . . . . . . . . . . . . . 15 (𝑓:ω⟶𝐴 → ran 𝑓𝐴)
2927, 28sstrid 3112 . . . . . . . . . . . . . 14 (𝑓:ω⟶𝐴 → (𝑓𝑛) ⊆ 𝐴)
3026, 29syl 14 . . . . . . . . . . . . 13 (𝑓:ω–onto𝐴 → (𝑓𝑛) ⊆ 𝐴)
3130ad2antrr 480 . . . . . . . . . . . 12 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → (𝑓𝑛) ⊆ 𝐴)
32313adantl1 1138 . . . . . . . . . . 11 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → (𝑓𝑛) ⊆ 𝐴)
33 simpl2 986 . . . . . . . . . . . . 13 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → 𝑓:ω–onto𝐴)
34 equequ1 1689 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (𝑥 = 𝑦𝑎 = 𝑦))
3534dcbid 824 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (DECID 𝑥 = 𝑦DECID 𝑎 = 𝑦))
36 equequ2 1690 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑏 → (𝑎 = 𝑦𝑎 = 𝑏))
3736dcbid 824 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 → (DECID 𝑎 = 𝑦DECID 𝑎 = 𝑏))
3835, 37cbvral2v 2668 . . . . . . . . . . . . . 14 (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ↔ ∀𝑎𝐴𝑏𝐴 DECID 𝑎 = 𝑏)
39 ssralv 3165 . . . . . . . . . . . . . . . . 17 ((𝑓𝑛) ⊆ 𝐴 → (∀𝑏𝐴 DECID 𝑎 = 𝑏 → ∀𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏))
4030, 39syl 14 . . . . . . . . . . . . . . . 16 (𝑓:ω–onto𝐴 → (∀𝑏𝐴 DECID 𝑎 = 𝑏 → ∀𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏))
4140ralimdv 2503 . . . . . . . . . . . . . . 15 (𝑓:ω–onto𝐴 → (∀𝑎𝐴𝑏𝐴 DECID 𝑎 = 𝑏 → ∀𝑎𝐴𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏))
42 ssralv 3165 . . . . . . . . . . . . . . 15 ((𝑓𝑛) ⊆ 𝐴 → (∀𝑎𝐴𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏 → ∀𝑎 ∈ (𝑓𝑛)∀𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏))
4330, 41, 42sylsyld 58 . . . . . . . . . . . . . 14 (𝑓:ω–onto𝐴 → (∀𝑎𝐴𝑏𝐴 DECID 𝑎 = 𝑏 → ∀𝑎 ∈ (𝑓𝑛)∀𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏))
4438, 43syl5bi 151 . . . . . . . . . . . . 13 (𝑓:ω–onto𝐴 → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 → ∀𝑎 ∈ (𝑓𝑛)∀𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏))
4533, 19, 44sylc 62 . . . . . . . . . . . 12 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∀𝑎 ∈ (𝑓𝑛)∀𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏)
46 simpr 109 . . . . . . . . . . . . . 14 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
47 fofun 5353 . . . . . . . . . . . . . . . . 17 (𝑓:ω–onto𝐴 → Fun 𝑓)
4847ad2antrr 480 . . . . . . . . . . . . . . . 16 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → Fun 𝑓)
49 ordom 4527 . . . . . . . . . . . . . . . . . . 19 Ord ω
50 ordtr 4307 . . . . . . . . . . . . . . . . . . 19 (Ord ω → Tr ω)
5149, 50ax-mp 5 . . . . . . . . . . . . . . . . . 18 Tr ω
52 trss 4042 . . . . . . . . . . . . . . . . . 18 (Tr ω → (𝑛 ∈ ω → 𝑛 ⊆ ω))
5351, 46, 52mpsyl 65 . . . . . . . . . . . . . . . . 17 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → 𝑛 ⊆ ω)
5426fdmd 5286 . . . . . . . . . . . . . . . . . 18 (𝑓:ω–onto𝐴 → dom 𝑓 = ω)
5554ad2antrr 480 . . . . . . . . . . . . . . . . 17 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → dom 𝑓 = ω)
5653, 55sseqtrrd 3140 . . . . . . . . . . . . . . . 16 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → 𝑛 ⊆ dom 𝑓)
57 fores 5361 . . . . . . . . . . . . . . . 16 ((Fun 𝑓𝑛 ⊆ dom 𝑓) → (𝑓𝑛):𝑛onto→(𝑓𝑛))
5848, 56, 57syl2anc 409 . . . . . . . . . . . . . . 15 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → (𝑓𝑛):𝑛onto→(𝑓𝑛))
59 vex 2692 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
6059resex 4867 . . . . . . . . . . . . . . . 16 (𝑓𝑛) ∈ V
61 foeq1 5348 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑓𝑛) → (𝑔:𝑛onto→(𝑓𝑛) ↔ (𝑓𝑛):𝑛onto→(𝑓𝑛)))
6260, 61spcev 2783 . . . . . . . . . . . . . . 15 ((𝑓𝑛):𝑛onto→(𝑓𝑛) → ∃𝑔 𝑔:𝑛onto→(𝑓𝑛))
6358, 62syl 14 . . . . . . . . . . . . . 14 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∃𝑔 𝑔:𝑛onto→(𝑓𝑛))
64 foeq2 5349 . . . . . . . . . . . . . . . 16 (𝑚 = 𝑛 → (𝑔:𝑚onto→(𝑓𝑛) ↔ 𝑔:𝑛onto→(𝑓𝑛)))
6564exbidv 1798 . . . . . . . . . . . . . . 15 (𝑚 = 𝑛 → (∃𝑔 𝑔:𝑚onto→(𝑓𝑛) ↔ ∃𝑔 𝑔:𝑛onto→(𝑓𝑛)))
6665rspcev 2792 . . . . . . . . . . . . . 14 ((𝑛 ∈ ω ∧ ∃𝑔 𝑔:𝑛onto→(𝑓𝑛)) → ∃𝑚 ∈ ω ∃𝑔 𝑔:𝑚onto→(𝑓𝑛))
6746, 63, 66syl2anc 409 . . . . . . . . . . . . 13 (((𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∃𝑚 ∈ ω ∃𝑔 𝑔:𝑚onto→(𝑓𝑛))
68673adantl1 1138 . . . . . . . . . . . 12 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∃𝑚 ∈ ω ∃𝑔 𝑔:𝑚onto→(𝑓𝑛))
69 fidcenum 6851 . . . . . . . . . . . 12 ((𝑓𝑛) ∈ Fin ↔ (∀𝑎 ∈ (𝑓𝑛)∀𝑏 ∈ (𝑓𝑛)DECID 𝑎 = 𝑏 ∧ ∃𝑚 ∈ ω ∃𝑔 𝑔:𝑚onto→(𝑓𝑛)))
7045, 68, 69sylanbrc 414 . . . . . . . . . . 11 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → (𝑓𝑛) ∈ Fin)
7124, 25, 32, 70inffinp1 11976 . . . . . . . . . 10 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∃𝑢𝐴 ¬ 𝑢 ∈ (𝑓𝑛))
72 simprl 521 . . . . . . . . . . . 12 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) → 𝑢𝐴)
73 foelrn 5661 . . . . . . . . . . . 12 ((𝑓:ω–onto𝐴𝑢𝐴) → ∃𝑘 ∈ ω 𝑢 = (𝑓𝑘))
7433, 72, 73syl2an2r 585 . . . . . . . . . . 11 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) → ∃𝑘 ∈ ω 𝑢 = (𝑓𝑘))
75 simpr 109 . . . . . . . . . . . . . 14 ((((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) ∧ 𝑘 ∈ ω) ∧ 𝑢 = (𝑓𝑘)) → 𝑢 = (𝑓𝑘))
76 simprr 522 . . . . . . . . . . . . . . 15 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) → ¬ 𝑢 ∈ (𝑓𝑛))
7776ad2antrr 480 . . . . . . . . . . . . . 14 ((((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) ∧ 𝑘 ∈ ω) ∧ 𝑢 = (𝑓𝑘)) → ¬ 𝑢 ∈ (𝑓𝑛))
7875, 77eqneltrrd 2237 . . . . . . . . . . . . 13 ((((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) ∧ 𝑘 ∈ ω) ∧ 𝑢 = (𝑓𝑘)) → ¬ (𝑓𝑘) ∈ (𝑓𝑛))
7978ex 114 . . . . . . . . . . . 12 (((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) ∧ 𝑘 ∈ ω) → (𝑢 = (𝑓𝑘) → ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
8079reximdva 2537 . . . . . . . . . . 11 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) → (∃𝑘 ∈ ω 𝑢 = (𝑓𝑘) → ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
8174, 80mpd 13 . . . . . . . . . 10 ((((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) ∧ (𝑢𝐴 ∧ ¬ 𝑢 ∈ (𝑓𝑛))) → ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))
8271, 81rexlimddv 2557 . . . . . . . . 9 (((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) ∧ 𝑛 ∈ ω) → ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))
8382ralrimiva 2508 . . . . . . . 8 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))
8418, 83jca 304 . . . . . . 7 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → (𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
85843com23 1188 . . . . . 6 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴𝑓:ω–onto𝐴) → (𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
86853expia 1184 . . . . 5 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴) → (𝑓:ω–onto𝐴 → (𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
8786eximdv 1853 . . . 4 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ω ≼ 𝐴) → (∃𝑓 𝑓:ω–onto𝐴 → ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛))))
8816, 17, 87sylc 62 . . 3 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → ∃𝑓(𝑓:ω–onto𝐴 ∧ ∀𝑛 ∈ ω ∃𝑘 ∈ ω ¬ (𝑓𝑘) ∈ (𝑓𝑛)))
8915, 88, 1sylanbrc 414 . 2 ((∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴) → 𝐴 ≈ ℕ)
9014, 89impbii 125 1 (𝐴 ≈ ℕ ↔ (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓 𝑓:ω–onto𝐴 ∧ ω ≼ 𝐴))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 820   ∧ w3a 963   = wceq 1332  ∃wex 1469   ∈ wcel 1481  ∀wral 2417  ∃wrex 2418   ⊆ wss 3075   class class class wbr 3936  Tr wtr 4033  Ord word 4291  ωcom 4511  dom cdm 4546  ran crn 4547   ↾ cres 4548   “ cima 4549  Fun wfun 5124  ⟶wf 5126  –onto→wfo 5128  ‘cfv 5130   ≈ cen 6639   ≼ cdom 6640  Fincfn 6641  ℕcn 8743 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-iinf 4509  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-addcom 7743  ax-addass 7745  ax-distr 7747  ax-i2m1 7748  ax-0lt1 7749  ax-0id 7751  ax-rnegex 7752  ax-cnre 7754  ax-pre-ltirr 7755  ax-pre-ltwlin 7756  ax-pre-lttrn 7757  ax-pre-ltadd 7759 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-iord 4295  df-on 4297  df-ilim 4298  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-riota 5737  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-recs 6209  df-frec 6295  df-1o 6320  df-er 6436  df-pm 6552  df-en 6642  df-dom 6643  df-fin 6644  df-dju 6930  df-inl 6939  df-inr 6940  df-case 6976  df-pnf 7825  df-mnf 7826  df-xr 7827  df-ltxr 7828  df-le 7829  df-sub 7958  df-neg 7959  df-inn 8744  df-n0 9001  df-z 9078  df-uz 9350  df-fz 9821  df-seqfrec 10249 This theorem is referenced by:  qnnen  11978
 Copyright terms: Public domain W3C validator