lmiclbs

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

	Ref	Expression
Hypotheses	lmimlbs.j	$⊢ J = LBasis (S)$
	lmimlbs.k	$⊢ K = LBasis (T)$
Assertion	lmiclbs	$⊢ S ≃_{𝑚} T \to (J \neq \emptyset \to K \neq \emptyset)$

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

Metamath Proof Explorer