Metamath Proof Explorer

Theorem acsmap2d

Description: In an algebraic closure system, if S and T have the same closure and S is independent, then there is a map f from T into the set of finite subsets of S such that S equals the union of ran f . This is proven by taking the map f from acsmapd and observing that, since S and T have the same closure, the closure of U. ran f must contain S . Since S is independent, by mrissmrcd , U. ran f must equal S . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses acsmap2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
acsmap2d.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
acsmap2d.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
acsmap2d.4 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
acsmap2d.5 ⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
acsmap2d.6 ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
Assertion acsmap2d ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) )

Proof

Step Hyp Ref Expression
1 acsmap2d.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2 acsmap2d.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 acsmap2d.3 ⊢ 𝐼 = ( mrInd ‘ 𝐴 )
4 acsmap2d.4 ⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
5 acsmap2d.5 ⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
6 acsmap2d.6 ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
7 1 acsmred ⊢ ( 𝜑 → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
8 3 7 4 mrissd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
9 7 2 5 mrcssidd ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑇 ) )
10 9 6 sseqtrrd ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑆 ) )
11 1 2 8 10 acsmapd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
13 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
14 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝑆 ∈ 𝐼 )
15 3 13 14 mrissd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝑆 ⊆ 𝑋 )
16 13 2 15 mrcssidd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝑆 ⊆ ( 𝑁 ‘ 𝑆 ) )
17 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
18 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
19 13 2 mrcssvd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ( 𝑁 ‘ ∪ ran 𝑓 ) ⊆ 𝑋 )
20 13 2 18 19 mrcssd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
21 frn ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ran 𝑓 ⊆ ( 𝒫 𝑆 ∩ Fin ) )
22 21 unissd ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ ∪ ( 𝒫 𝑆 ∩ Fin ) )
23 unifpw ⊢ ∪ ( 𝒫 𝑆 ∩ Fin ) = 𝑆
24 22 23 sseqtrdi ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ 𝑆 )
25 24 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ∪ ran 𝑓 ⊆ 𝑆 )
26 25 15 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ∪ ran 𝑓 ⊆ 𝑋 )
27 13 2 26 mrcidmd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ( 𝑁 ‘ ( 𝑁 ‘ ∪ ran 𝑓 ) ) = ( 𝑁 ‘ ∪ ran 𝑓 ) )
28 20 27 sseqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ( 𝑁 ‘ 𝑇 ) ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
29 17 28 eqsstrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ( 𝑁 ‘ 𝑆 ) ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
30 16 29 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝑆 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
31 13 2 3 30 25 14 mrissmrcd ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → 𝑆 = ∪ ran 𝑓 )
32 12 31 jca ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) )
33 32 ex ⊢ ( 𝜑 → ( ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) )
34 33 eximdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) )
35 11 34 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) )