This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem acsdomd

Description: In an algebraic closure system, if S and T have the same closure and S is infinite independent, then T dominates S . This follows from applying acsinfd and then applying unirnfdomd to the map given in acsmap2d . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses acsmap2d.1 ⊢ φ → A ∈ ACS ⁡ X
acsmap2d.2 ⊢ N = mrCls ⁡ A
acsmap2d.3 ⊢ I = mrInd ⁡ A
acsmap2d.4 ⊢ φ → S ∈ I
acsmap2d.5 ⊢ φ → T ⊆ X
acsmap2d.6 ⊢ φ → N ⁡ S = N ⁡ T
acsinfd.7 ⊢ φ → ¬ S ∈ Fin
Assertion acsdomd ⊢ φ → S ≼ T

Proof

Step Hyp Ref Expression
1 acsmap2d.1 ⊢ φ → A ∈ ACS ⁡ X
2 acsmap2d.2 ⊢ N = mrCls ⁡ A
3 acsmap2d.3 ⊢ I = mrInd ⁡ A
4 acsmap2d.4 ⊢ φ → S ∈ I
5 acsmap2d.5 ⊢ φ → T ⊆ X
6 acsmap2d.6 ⊢ φ → N ⁡ S = N ⁡ T
7 acsinfd.7 ⊢ φ → ¬ S ∈ Fin
8 1 2 3 4 5 6 acsmap2d ⊢ φ → ∃ f f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f
9 simprr ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → S = ⋃ ran ⁡ f
10 simprl ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → f : T ⟶ 𝒫 S ∩ Fin
11 inss2 ⊢ 𝒫 S ∩ Fin ⊆ Fin
12 fss ⊢ f : T ⟶ 𝒫 S ∩ Fin ∧ 𝒫 S ∩ Fin ⊆ Fin → f : T ⟶ Fin
13 10 11 12 sylancl ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → f : T ⟶ Fin
14 1 2 3 4 5 6 7 acsinfd ⊢ φ → ¬ T ∈ Fin
15 14 adantr ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → ¬ T ∈ Fin
16 1 adantr ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → A ∈ ACS ⁡ X
17 16 elfvexd ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → X ∈ V
18 5 adantr ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → T ⊆ X
19 17 18 ssexd ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → T ∈ V
20 13 15 19 unirnfdomd ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → ⋃ ran ⁡ f ≼ T
21 9 20 eqbrtrd ⊢ φ ∧ f : T ⟶ 𝒫 S ∩ Fin ∧ S = ⋃ ran ⁡ f → S ≼ T
22 8 21 exlimddv ⊢ φ → S ≼ T