Theorem 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	$$⊢\phi \to A\in \mathrm{ACS}\left(X\right)$$
	acsmap2d.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
	acsmap2d.3	$$⊢I=\mathrm{mrInd}\left(A\right)$$
	acsmap2d.4	$$⊢\phi \to S\in I$$
	acsmap2d.5	$$⊢\phi \to T\subseteq X$$
	acsmap2d.6	$$⊢\phi \to N\left(S\right)=N\left(T\right)$$
	acsinfd.7	$$⊢\phi \to \neg S\in \mathrm{Fin}$$
Assertion	acsdomd	$$⊢\phi \to S\preccurlyeq T$$

Proof

Step	Hyp	Ref	Expression
1		acsmap2d.1	$$⊢\phi \to A\in \mathrm{ACS}\left(X\right)$$
2		acsmap2d.2	$$⊢N=\mathrm{mrCls}\left(A\right)$$
3		acsmap2d.3	$$⊢I=\mathrm{mrInd}\left(A\right)$$
4		acsmap2d.4	$$⊢\phi \to S\in I$$
5		acsmap2d.5	$$⊢\phi \to T\subseteq X$$
6		acsmap2d.6	$$⊢\phi \to N\left(S\right)=N\left(T\right)$$
7		acsinfd.7	$$⊢\phi \to \neg S\in \mathrm{Fin}$$
8	1 2 3 4 5 6	acsmap2d	$$⊢\phi \to \exists f\left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)$$
9		simprr	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to S=\bigcup \mathrm{ran}f$$
10		simprl	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to f:T⟶𝒫S\cap \mathrm{Fin}$$
11		inss2	$$⊢𝒫S\cap \mathrm{Fin}\subseteq \mathrm{Fin}$$
12		fss	$$⊢\left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge 𝒫S\cap \mathrm{Fin}\subseteq \mathrm{Fin}\right)\to f:T⟶\mathrm{Fin}$$
13	10 11 12	sylancl	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to f:T⟶\mathrm{Fin}$$
14	1 2 3 4 5 6 7	acsinfd	$$⊢\phi \to \neg T\in \mathrm{Fin}$$
15	14	adantr	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to \neg T\in \mathrm{Fin}$$
16	1	adantr	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to A\in \mathrm{ACS}\left(X\right)$$
17	16	elfvexd	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to X\in \mathrm{V}$$
18	5	adantr	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to T\subseteq X$$
19	17 18	ssexd	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to T\in \mathrm{V}$$
20	13 15 19	unirnfdomd	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to \bigcup \mathrm{ran}f\preccurlyeq T$$
21	9 20	eqbrtrd	$$⊢\left(\phi \wedge \left(f:T⟶𝒫S\cap \mathrm{Fin}\wedge S=\bigcup \mathrm{ran}f\right)\right)\to S\preccurlyeq T$$
22	8 21	exlimddv	$$⊢\phi \to S\preccurlyeq T$$