This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrid ⊢ ( 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( 𝐽 ≠ ∅ → 𝐾 ≠ ∅ ) )
12 11 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑆 LMIso 𝑇 ) → ( 𝐽 ≠ ∅ → 𝐾 ≠ ∅ ) )
13 5 12 sylbi ⊢ ( 𝑆 ≃𝑚 𝑇 → ( 𝐽 ≠ ∅ → 𝐾 ≠ ∅ ) )