infinfnum - Mathbox for BTernaryTau

	Mathbox for BTernaryTau		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > infinfnum		Structured version Visualization version GIF version

Theorem infinfnum 35890

Description: Equivalence between two infiniteness criteria for numerable sets. (Contributed by BTernaryTau, 15-Jul-2026.)

**Assertion**
Ref	Expression
infinfnum	⊢ (𝐴 ∈ dom card → (¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴))

**Proof of Theorem infinfnum**
Step	Hyp	Ref	Expression
1		isfin4-2 10431	. . 3 ⊢ (𝐴 ∈ dom card → (𝐴 ∈ Fin^IV ↔ ¬ ω ≼ 𝐴))
2	1	con2bid 357	. 2 ⊢ (𝐴 ∈ dom card → (ω ≼ 𝐴 ↔ ¬ 𝐴 ∈ Fin^IV))
3		fin45 10509	. . . . . 6 ⊢ (𝐴 ∈ Fin^IV → 𝐴 ∈ Fin^V)
4		fin56 10510	. . . . . 6 ⊢ (𝐴 ∈ Fin^V → 𝐴 ∈ Fin^VI)
5		fin67 10512	. . . . . 6 ⊢ (𝐴 ∈ Fin^VI → 𝐴 ∈ Fin^VII)
6	3, 4, 5	3syl 19	. . . . 5 ⊢ (𝐴 ∈ Fin^IV → 𝐴 ∈ Fin^VII)
7		fin71num 10514	. . . . 5 ⊢ (𝐴 ∈ dom card → (𝐴 ∈ Fin^VII ↔ 𝐴 ∈ Fin))
8	6, 7	imbitrid 247	. . . 4 ⊢ (𝐴 ∈ dom card → (𝐴 ∈ Fin^IV → 𝐴 ∈ Fin))
9		fin12 10530	. . . . 5 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ Fin^II)
10		fin23 10506	. . . . 5 ⊢ (𝐴 ∈ Fin^II → 𝐴 ∈ Fin^III)
11		fin34 10507	. . . . 5 ⊢ (𝐴 ∈ Fin^III → 𝐴 ∈ Fin^IV)
12	9, 10, 11	3syl 19	. . . 4 ⊢ (𝐴 ∈ Fin → 𝐴 ∈ Fin^IV)
13	8, 12	impbid1 228	. . 3 ⊢ (𝐴 ∈ dom card → (𝐴 ∈ Fin^IV ↔ 𝐴 ∈ Fin))
14	13	notbid 321	. 2 ⊢ (𝐴 ∈ dom card → (¬ 𝐴 ∈ Fin^IV ↔ ¬ 𝐴 ∈ Fin))
15	2, 14	bitr2d 283	1 ⊢ (𝐴 ∈ dom card → (¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∈ wcel 2147 class class class wbr 5108 dom cdm 5658 ωcom 7911 ≼ cdom 9009 Fincfn 9011 cardccrd 10053 Fin^IIcfin2 10396 Fin^IVcfin4 10397 Fin^IIIcfin3 10398 Fin^Vcfin5 10399 Fin^VIcfin6 10400 Fin^VIIcfin7 10401

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-inf2 9679

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-se 5612 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-isom 6575 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-rpss 7771 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-seqom 8496 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-oi 9541 df-wdom 9596 df-dju 10019 df-card 10057 df-fin2 10403 df-fin4 10404 df-fin3 10405 df-fin5 10406 df-fin6 10407 df-fin7 10408

This theorem is used by: acwer1prc 35893 j0ltaleph 36049 jltaleph 36067

W3C validator