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 ⊢ J = LBasis ⁡ S
lmimlbs.k ⊢ K = LBasis ⁡ T
Assertion lmiclbs ⊢ S ≃ 𝑚 T → J ≠ ∅ → K ≠ ∅

Proof

Step Hyp Ref Expression
1 lmimlbs.j ⊢ J = LBasis ⁡ S
2 lmimlbs.k ⊢ K = LBasis ⁡ T
3 brlmic ⊢ S ≃ 𝑚 T ↔ S LMIso T ≠ ∅
4 n0 ⊢ S LMIso T ≠ ∅ ↔ ∃ f f ∈ S LMIso T
5 3 4 bitri ⊢ S ≃ 𝑚 T ↔ ∃ f f ∈ S LMIso T
6 n0 ⊢ J ≠ ∅ ↔ ∃ b b ∈ J
7 1 2 lmimlbs ⊢ f ∈ S LMIso T ∧ b ∈ J → f b ∈ K
8 7 ne0d ⊢ f ∈ S LMIso T ∧ b ∈ J → K ≠ ∅
9 8 ex ⊢ f ∈ S LMIso T → b ∈ J → K ≠ ∅
10 9 exlimdv ⊢ f ∈ S LMIso T → ∃ b b ∈ J → K ≠ ∅
11 6 10 syl5bi ⊢ f ∈ S LMIso T → J ≠ ∅ → K ≠ ∅
12 11 exlimiv ⊢ ∃ f f ∈ S LMIso T → J ≠ ∅ → K ≠ ∅
13 5 12 sylbi ⊢ S ≃ 𝑚 T → J ≠ ∅ → K ≠ ∅