Theorem acsinfdimd 18492

Description: In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 18491 twice with acsinfd 18490. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
acsinfdimd.1	⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))
acsinfdimd.2	⊢ 𝑁 = (mrCls‘𝐴)
acsinfdimd.3	⊢ 𝐼 = (mrInd‘𝐴)
acsinfdimd.4	⊢ (𝜑 → 𝑆 ∈ 𝐼)
acsinfdimd.5	⊢ (𝜑 → 𝑇 ∈ 𝐼)
acsinfdimd.6	⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))
acsinfdimd.7	⊢ (𝜑 → ¬ 𝑆 ∈ Fin)

Assertion

Ref	Expression
acsinfdimd	⊢ (𝜑 → 𝑆 ≈ 𝑇)

Proof of Theorem acsinfdimd

Step	Hyp	Ref	Expression
1		acsinfdimd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋))
2		acsinfdimd.2	. . 3 ⊢ 𝑁 = (mrCls‘𝐴)
3		acsinfdimd.3	. . 3 ⊢ 𝐼 = (mrInd‘𝐴)
4		acsinfdimd.4	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝐼)
5	1	acsmred 17581	. . . 4 ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
6		acsinfdimd.5	. . . 4 ⊢ (𝜑 → 𝑇 ∈ 𝐼)
7	3, 5, 6	mrissd 17561	. . 3 ⊢ (𝜑 → 𝑇 ⊆ 𝑋)
8		acsinfdimd.6	. . 3 ⊢ (𝜑 → (𝑁‘𝑆) = (𝑁‘𝑇))
9		acsinfdimd.7	. . 3 ⊢ (𝜑 → ¬ 𝑆 ∈ Fin)
10	1, 2, 3, 4, 7, 8, 9	acsdomd 18491	. 2 ⊢ (𝜑 → 𝑆 ≼ 𝑇)
11	3, 5, 4	mrissd 17561	. . 3 ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
12	8	eqcomd 2737	. . 3 ⊢ (𝜑 → (𝑁‘𝑇) = (𝑁‘𝑆))
13	1, 2, 3, 4, 7, 8, 9	acsinfd 18490	. . 3 ⊢ (𝜑 → ¬ 𝑇 ∈ Fin)
14	1, 2, 3, 6, 11, 12, 13	acsdomd 18491	. 2 ⊢ (𝜑 → 𝑇 ≼ 𝑆)
15		sbth 9075	. 2 ⊢ ((𝑆 ≼ 𝑇 ∧ 𝑇 ≼ 𝑆) → 𝑆 ≈ 𝑇)
16	10, 14, 15	syl2anc 584	1 ⊢ (𝜑 → 𝑆 ≈ 𝑇)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2106   class class class wbr 5140  ‘cfv 6531   ≈ cen 8918   ≼ cdom 8919  Fincfn 8921  mrClscmrc 17508  mrIndcmri 17509  ACScacs 17510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5277  ax-sep 5291  ax-nul 5298  ax-pow 5355  ax-pr 5419  ax-un 7707  ax-reg 9568  ax-inf2 9617  ax-ac2 10439  ax-cnex 11147  ax-resscn 11148  ax-1cn 11149  ax-icn 11150  ax-addcl 11151  ax-addrcl 11152  ax-mulcl 11153  ax-mulrcl 11154  ax-mulcom 11155  ax-addass 11156  ax-mulass 11157  ax-distr 11158  ax-i2m1 11159  ax-1ne0 11160  ax-1rid 11161  ax-rnegex 11162  ax-rrecex 11163  ax-cnre 11164  ax-pre-lttri 11165  ax-pre-lttrn 11166  ax-pre-ltadd 11167  ax-pre-mulgt0 11168

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3474  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-int 4943  df-iun 4991  df-iin 4992  df-br 5141  df-opab 5203  df-mpt 5224  df-tr 5258  df-id 5566  df-eprel 5572  df-po 5580  df-so 5581  df-fr 5623  df-se 5624  df-we 5625  df-xp 5674  df-rel 5675  df-cnv 5676  df-co 5677  df-dm 5678  df-rn 5679  df-res 5680  df-ima 5681  df-pred 6288  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6483  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-isom 6540  df-riota 7348  df-ov 7395  df-oprab 7396  df-mpo 7397  df-om 7838  df-1st 7956  df-2nd 7957  df-frecs 8247  df-wrecs 8278  df-recs 8352  df-rdg 8391  df-1o 8447  df-er 8685  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-oi 9486  df-r1 9740  df-rank 9741  df-card 9915  df-acn 9918  df-ac 10092  df-pnf 11231  df-mnf 11232  df-xr 11233  df-ltxr 11234  df-le 11235  df-sub 11427  df-neg 11428  df-nn 12194  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261  df-8 12262  df-9 12263  df-n0 12454  df-z 12540  df-dec 12659  df-uz 12804  df-fz 13466  df-struct 17061  df-slot 17096  df-ndx 17108  df-base 17126  df-tset 17197  df-ple 17198  df-ocomp 17199  df-mre 17511  df-mrc 17512  df-mri 17513  df-acs 17514  df-proset 18229  df-drs 18230  df-poset 18247  df-ipo 18462

This theorem is referenced by:  acsexdimd  18493