Theorem lmiclbs

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

	Ref	Expression
Hypotheses	lmimlbs.j	⊢ 𝐽 = ( LBasis ‘ 𝑆 )
	lmimlbs.k	⊢ 𝐾 = ( LBasis ‘ 𝑇 )
Assertion	lmiclbs	⊢ ( 𝑆 ≃𝑚 𝑇 → ( 𝐽 ≠ ∅ → 𝐾 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		lmimlbs.j	⊢ 𝐽 = ( LBasis ‘ 𝑆 )
2		lmimlbs.k	⊢ 𝐾 = ( LBasis ‘ 𝑇 )
3		brlmic	⊢ ( 𝑆 ≃𝑚 𝑇 ↔ ( 𝑆 LMIso 𝑇 ) ≠ ∅ )
4		n0	⊢ ( ( 𝑆 LMIso 𝑇 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) )
5	3 4	bitri	⊢ ( 𝑆 ≃𝑚 𝑇 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) )
6		n0	⊢ ( 𝐽 ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ 𝐽 )
7	1 2	lmimlbs	⊢ ( ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝑏 ∈ 𝐽 ) → ( 𝑓 “ 𝑏 ) ∈ 𝐾 )
8	7	ne0d	⊢ ( ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) ∧ 𝑏 ∈ 𝐽 ) → 𝐾 ≠ ∅ )
9	8	ex	⊢ ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( 𝑏 ∈ 𝐽 → 𝐾 ≠ ∅ ) )
10	9	exlimdv	⊢ ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( ∃ 𝑏 𝑏 ∈ 𝐽 → 𝐾 ≠ ∅ ) )
11	6 10	syl5bi	⊢ ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( 𝐽 ≠ ∅ → 𝐾 ≠ ∅ ) )
12	11	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( 𝐽 ≠ ∅ → 𝐾 ≠ ∅ ) )
13	5 12	sylbi	⊢ ( 𝑆 ≃𝑚 𝑇 → ( 𝐽 ≠ ∅ → 𝐾 ≠ ∅ ) )