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	⊢ ( 𝜑 → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
	acsmap2d.2	⊢ 𝑁 = ( mrCls ‘ 𝐴 )
	acsmap2d.3	⊢ 𝐼 = ( mrInd ‘ 𝐴 )
	acsmap2d.4	⊢ ( 𝜑 → 𝑆 ∈ 𝐼 )
	acsmap2d.5	⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
	acsmap2d.6	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑆 ) = ( 𝑁 ‘ 𝑇 ) )
	acsinfd.7	⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )
Assertion	acsdomd	⊢ ( 𝜑 → 𝑆 ≼ 𝑇 )

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		acsinfd.7	⊢ ( 𝜑 → ¬ 𝑆 ∈ Fin )
8	1 2 3 4 5 6	acsmap2d	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) )
9		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝑆 = ∪ ran 𝑓 )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) )
11		inss2	⊢ ( 𝒫 𝑆 ∩ Fin ) ⊆ Fin
12		fss	⊢ ( ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ ( 𝒫 𝑆 ∩ Fin ) ⊆ Fin ) → 𝑓 : 𝑇 ⟶ Fin )
13	10 11 12	sylancl	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝑓 : 𝑇 ⟶ Fin )
14	1 2 3 4 5 6 7	acsinfd	⊢ ( 𝜑 → ¬ 𝑇 ∈ Fin )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → ¬ 𝑇 ∈ Fin )
16	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝐴 ∈ ( ACS ‘ 𝑋 ) )
17	16	elfvexd	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝑋 ∈ V )
18	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝑇 ⊆ 𝑋 )
19	17 18	ssexd	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝑇 ∈ V )
20	13 15 19	unirnfdomd	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → ∪ ran 𝑓 ≼ 𝑇 )
21	9 20	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝑓 : 𝑇 ⟶ ( 𝒫 𝑆 ∩ Fin ) ∧ 𝑆 = ∪ ran 𝑓 ) ) → 𝑆 ≼ 𝑇 )
22	8 21	exlimddv	⊢ ( 𝜑 → 𝑆 ≼ 𝑇 )

Metamath Proof Explorer

Theorem acsdomd

Proof