Theorem lmiclbs

Description: Having a basis is an isomorphism invariant. (Contributed by Stefan O'Rear, 26-Feb-2015)

	Ref	Expression
Hypotheses	lmimlbs.j	$$⊢J=\mathrm{LBasis}\left(S\right)$$
	lmimlbs.k	$$⊢K=\mathrm{LBasis}\left(T\right)$$
Assertion	lmiclbs	$$⊢S{\simeq }_{𝑚}T\to \left(J\ne \varnothing \to K\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		lmimlbs.j	$$⊢J=\mathrm{LBasis}\left(S\right)$$
2		lmimlbs.k	$$⊢K=\mathrm{LBasis}\left(T\right)$$
3		brlmic	$$⊢S{\simeq }_{𝑚}T\leftrightarrow S\mathrm{LMIso}T\ne \varnothing$$
4		n0	$$⊢S\mathrm{LMIso}T\ne \varnothing \leftrightarrow \exists ff\in \left(S\mathrm{LMIso}T\right)$$
5	3 4	bitri	$$⊢S{\simeq }_{𝑚}T\leftrightarrow \exists ff\in \left(S\mathrm{LMIso}T\right)$$
6		n0	$$⊢J\ne \varnothing \leftrightarrow \exists bb\in J$$
7	1 2	lmimlbs	$$⊢\left(f\in \left(S\mathrm{LMIso}T\right)\wedge b\in J\right)\to f\left[b\right]\in K$$
8	7	ne0d	$$⊢\left(f\in \left(S\mathrm{LMIso}T\right)\wedge b\in J\right)\to K\ne \varnothing$$
9	8	ex	$$⊢f\in \left(S\mathrm{LMIso}T\right)\to \left(b\in J\to K\ne \varnothing \right)$$
10	9	exlimdv	$$⊢f\in \left(S\mathrm{LMIso}T\right)\to \left(\exists bb\in J\to K\ne \varnothing \right)$$
11	6 10	biimtrid	$$⊢f\in \left(S\mathrm{LMIso}T\right)\to \left(J\ne \varnothing \to K\ne \varnothing \right)$$
12	11	exlimiv	$$⊢\exists ff\in \left(S\mathrm{LMIso}T\right)\to \left(J\ne \varnothing \to K\ne \varnothing \right)$$
13	5 12	sylbi	$$⊢S{\simeq }_{𝑚}T\to \left(J\ne \varnothing \to K\ne \varnothing \right)$$