Metamath Proof Explorer

Theorem acsmapd

Description: In an algebraic closure system, if T is contained in the closure of S , there is a map f from T into the set of finite subsets of S such that the closure of U. ran f contains T . This is proven by applying acsficl2d to each element of T . See Section II.5 in Cohn p. 81 to 82. (Contributed by David Moews, 1-May-2017)

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

Proof

Step Hyp Ref Expression
1 acsmapd.1 ⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
2 acsmapd.2 ⊢ 𝑁 = ( mrCls ‘ 𝐴 )
3 acsmapd.3 ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
4 acsmapd.4 ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑁 ‘ 𝑆 ) )
5 fvex ⊢ ( 𝑁 ‘ 𝑆 ) ∈ V
6 5 ssex ⊢ ( 𝑇 ⊆ ( 𝑁 ‘ 𝑆 ) → 𝑇 ∈ V )
7 4 6 syl ⊢ ( 𝜑 → 𝑇 ∈ V )
8 4 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) ) )
9 1 2 3 acsficl2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ) )
10 8 9 sylibd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ) )
11 10 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) )
12 fveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
13 12 eleq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
14 13 ac6sg ⊢ ( 𝑇 ∈ V → ( ∀ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) )
15 7 11 14 sylc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
17 nfv ⊢ Ⅎ 𝑥 𝜑
18 nfv ⊢ Ⅎ 𝑥 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin )
19 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) )
20 18 19 nfan ⊢ Ⅎ 𝑥 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
21 17 20 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
22 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
23 22 acsmred ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
24 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
25 24 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑓 Fn 𝑇 )
26 fnfvelrn ⊢ ( ( 𝑓 Fn 𝑇 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
27 25 26 sylancom ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
28 27 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → { ( 𝑓 ‘ 𝑥 ) } ⊆ ran 𝑓 )
29 28 unissd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ { ( 𝑓 ‘ 𝑥 ) } ⊆ ∪ ran 𝑓 )
30 frn ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ran 𝑓 ⊆ ( 𝒫 𝑆 ∩ Fin ) )
31 30 unissd ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ ∪ ( 𝒫 𝑆 ∩ Fin ) )
32 unifpw ⊢ ∪ ( 𝒫 𝑆 ∩ Fin ) = 𝑆
33 31 32 sseqtrdi ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ 𝑆 )
34 24 33 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ ran 𝑓 ⊆ 𝑆 )
35 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑆 ⊆ 𝑋 )
36 34 35 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ ran 𝑓 ⊆ 𝑋 )
37 23 2 29 36 mrcssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
38 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
39 38 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
40 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
41 40 unisn ⊢ ∪ { ( 𝑓 ‘ 𝑥 ) } = ( 𝑓 ‘ 𝑥 )
42 41 fveq2i ⊢ ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) )
43 39 42 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) )
44 37 43 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) )
45 44 ex ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
46 21 45 alrimi ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
47 dfss2 ⊢ ( 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
48 46 47 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
49 16 48 jca ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
50 49 ex ⊢ ( 𝜑 → ( ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) )
51 50 eximdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) )
52 15 51 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )