Theorem fin0or 6997

Description: A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.)

Assertion

Ref	Expression
fin0or	⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ∃𝑥 𝑥 ∈ 𝐴))

Distinct variable group:   𝑥,𝐴

Proof of Theorem fin0or

Dummy variables 𝑓 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfi 6864	. . 3 ⊢ (𝐴 ∈ Fin ↔ ∃𝑛 ∈ ω 𝐴 ≈ 𝑛)
2	1	biimpi 120	. 2 ⊢ (𝐴 ∈ Fin → ∃𝑛 ∈ ω 𝐴 ≈ 𝑛)
3		nn0suc 4659	. . . 4 ⊢ (𝑛 ∈ ω → (𝑛 = ∅ ∨ ∃𝑚 ∈ ω 𝑛 = suc 𝑚))
4	3	ad2antrl 490	. . 3 ⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝑛 = ∅ ∨ ∃𝑚 ∈ ω 𝑛 = suc 𝑚))
5		simplrr 536	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 ≈ 𝑛)
6		simpr 110	. . . . . . 7 ⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝑛 = ∅)
7	5, 6	breqtrd 4076	. . . . . 6 ⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 ≈ ∅)
8		en0 6899	. . . . . 6 ⊢ (𝐴 ≈ ∅ ↔ 𝐴 = ∅)
9	7, 8	sylib 122	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑛 = ∅) → 𝐴 = ∅)
10	9	ex 115	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝑛 = ∅ → 𝐴 = ∅))
11		simplrr 536	. . . . . . . . . 10 ⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) → 𝐴 ≈ 𝑛)
12	11	adantr 276	. . . . . . . . 9 ⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → 𝐴 ≈ 𝑛)
13	12	ensymd 6887	. . . . . . . 8 ⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → 𝑛 ≈ 𝐴)
14		bren 6847	. . . . . . . 8 ⊢ (𝑛 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝑛–1-1-onto→𝐴)
15	13, 14	sylib 122	. . . . . . 7 ⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → ∃𝑓 𝑓:𝑛–1-1-onto→𝐴)
16		f1of 5533	. . . . . . . . . 10 ⊢ (𝑓:𝑛–1-1-onto→𝐴 → 𝑓:𝑛⟶𝐴)
17	16	adantl 277	. . . . . . . . 9 ⊢ (((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑓:𝑛⟶𝐴)
18		sucidg 4470	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ω → 𝑚 ∈ suc 𝑚)
19	18	ad3antlr 493	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑚 ∈ suc 𝑚)
20		simplr 528	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑛 = suc 𝑚)
21	19, 20	eleqtrrd 2286	. . . . . . . . 9 ⊢ (((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → 𝑚 ∈ 𝑛)
22	17, 21	ffvelcdmd 5728	. . . . . . . 8 ⊢ (((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → (𝑓‘𝑚) ∈ 𝐴)
23		elex2 2790	. . . . . . . 8 ⊢ ((𝑓‘𝑚) ∈ 𝐴 → ∃𝑥 𝑥 ∈ 𝐴)
24	22, 23	syl 14	. . . . . . 7 ⊢ (((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) ∧ 𝑓:𝑛–1-1-onto→𝐴) → ∃𝑥 𝑥 ∈ 𝐴)
25	15, 24	exlimddv 1923	. . . . . 6 ⊢ ((((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) ∧ 𝑛 = suc 𝑚) → ∃𝑥 𝑥 ∈ 𝐴)
26	25	ex 115	. . . . 5 ⊢ (((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) ∧ 𝑚 ∈ ω) → (𝑛 = suc 𝑚 → ∃𝑥 𝑥 ∈ 𝐴))
27	26	rexlimdva 2624	. . . 4 ⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (∃𝑚 ∈ ω 𝑛 = suc 𝑚 → ∃𝑥 𝑥 ∈ 𝐴))
28	10, 27	orim12d 788	. . 3 ⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → ((𝑛 = ∅ ∨ ∃𝑚 ∈ ω 𝑛 = suc 𝑚) → (𝐴 = ∅ ∨ ∃𝑥 𝑥 ∈ 𝐴)))
29	4, 28	mpd 13	. 2 ⊢ ((𝐴 ∈ Fin ∧ (𝑛 ∈ ω ∧ 𝐴 ≈ 𝑛)) → (𝐴 = ∅ ∨ ∃𝑥 𝑥 ∈ 𝐴))
30	2, 29	rexlimddv 2629	1 ⊢ (𝐴 ∈ Fin → (𝐴 = ∅ ∨ ∃𝑥 𝑥 ∈ 𝐴))

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 710   = wceq 1373  ∃wex 1516   ∈ wcel 2177  ∃wrex 2486  ∅c0 3464   class class class wbr 4050  suc csuc 4419  ωcom 4645  ⟶wf 5275  –1-1-onto→wf1o 5278  ‘cfv 5279   ≈ cen 6837  Fincfn 6839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4169  ax-nul 4177  ax-pow 4225  ax-pr 4260  ax-un 4487  ax-iinf 4643

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3003  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-nul 3465  df-pw 3622  df-sn 3643  df-pr 3644  df-op 3646  df-uni 3856  df-int 3891  df-br 4051  df-opab 4113  df-id 4347  df-suc 4425  df-iom 4646  df-xp 4688  df-rel 4689  df-cnv 4690  df-co 4691  df-dm 4692  df-rn 4693  df-res 4694  df-ima 4695  df-iota 5240  df-fun 5281  df-fn 5282  df-f 5283  df-f1 5284  df-fo 5285  df-f1o 5286  df-fv 5287  df-er 6632  df-en 6840  df-fin 6842

This theorem is referenced by:  xpfi  7043  fival  7086  fiubm  10990  lswex  11062  fsumcllem  11780  fprodcllem  11987  gsumwsubmcl  13398  gsumwmhm  13400