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 𝑓 ) )

Metamath Proof Explorer

Theorem acsmap2d

Proof