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) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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 1 elfvexd ⊢ ( 𝜑 → 𝑋 ∈ V )
9 8 3 ssexd ⊢ ( 𝜑 → 𝑆 ∈ V )
10 9 pwexd ⊢ ( 𝜑 → 𝒫 𝑆 ∈ V )
11 inex1g ⊢ ( 𝒫 𝑆 ∈ V → ( 𝒫 𝑆 ∩ Fin ) ∈ V )
12 10 11 syl ⊢ ( 𝜑 → ( 𝒫 𝑆 ∩ Fin ) ∈ V )
13 4 sseld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) ) )
14 1 2 3 acsficl2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑁 ‘ 𝑆 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ) )
15 13 14 sylibd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑇 → ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ) )
16 15 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) )
17 fveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
18 17 eleq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ↔ 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
19 18 ac6 ⊢ ( ( 𝑇 ∈ V ∧ ( 𝒫 𝑆 ∩ Fin ) ∈ V ∧ ∀ 𝑥 ∈ 𝑇 ∃ 𝑦 ∈ ( 𝒫 𝑆 ∩ Fin ) 𝑥 ∈ ( 𝑁 ‘ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
20 7 12 16 19 syl3anc ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
22 nfv ⊢ Ⅎ 𝑥 𝜑
23 nfv ⊢ Ⅎ 𝑥 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin )
24 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) )
25 23 24 nfan ⊢ Ⅎ 𝑥 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
26 22 25 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) )
27 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
28 27 acsmred ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝐴 ∈ ( Moore ‘ 𝑋 ) )
29 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
30 29 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑓 Fn 𝑇 )
31 fnfvelrn ⊢ ( ( 𝑓 Fn 𝑇 ∧ 𝑥 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
32 30 31 sylancom ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑓 ‘ 𝑥 ) ∈ ran 𝑓 )
33 32 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → { ( 𝑓 ‘ 𝑥 ) } ⊆ ran 𝑓 )
34 33 unissd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ { ( 𝑓 ‘ 𝑥 ) } ⊆ ∪ ran 𝑓 )
35 frn ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ran 𝑓 ⊆ ( 𝒫 𝑆 ∩ Fin ) )
36 35 unissd ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ ∪ ( 𝒫 𝑆 ∩ Fin ) )
37 unifpw ⊢ ∪ ( 𝒫 𝑆 ∩ Fin ) = 𝑆
38 36 37 sseqtrdi ⊢ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) → ∪ ran 𝑓 ⊆ 𝑆 )
39 29 38 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ ran 𝑓 ⊆ 𝑆 )
40 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑆 ⊆ 𝑋 )
41 39 40 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ∪ ran 𝑓 ⊆ 𝑋 )
42 28 2 34 41 mrcssd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
43 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
44 43 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) )
45 fvex ⊢ ( 𝑓 ‘ 𝑥 ) ∈ V
46 45 unisn ⊢ ∪ { ( 𝑓 ‘ 𝑥 ) } = ( 𝑓 ‘ 𝑥 )
47 46 fveq2i ⊢ ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) = ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) )
48 44 47 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ∪ { ( 𝑓 ‘ 𝑥 ) } ) )
49 42 48 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) ∧ 𝑥 ∈ 𝑇 ) → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) )
50 49 ex ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
51 26 50 alrimi ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
52 df-ss ⊢ ( 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑇 → 𝑥 ∈ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
53 51 52 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) )
54 21 53 jca ⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )
55 54 ex ⊢ ( 𝜑 → ( ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) → ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) )
56 55 eximdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ∀ 𝑥 ∈ 𝑇 𝑥 ∈ ( 𝑁 ‘ ( 𝑓 ‘ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) ) )
57 20 56 mpd ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑇 ⊆ ( 𝑁 ‘ ∪ ran 𝑓 ) ) )