Metamath Proof Explorer

Theorem lspexchn2

Description: Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch to see if this will shorten proofs. (Contributed by NM, 24-May-2015)

Ref Expression
Hypotheses lspexchn2.v ⊢ V = Base W
lspexchn2.n ⊢ N = LSpan ⁡ W
lspexchn2.w ⊢ φ → W ∈ LVec
lspexchn2.x ⊢ φ → X ∈ V
lspexchn2.y ⊢ φ → Y ∈ V
lspexchn2.z ⊢ φ → Z ∈ V
lspexchn2.q ⊢ φ → ¬ Y ∈ N ⁡ Z
lspexchn2.e ⊢ φ → ¬ X ∈ N ⁡ Z Y
Assertion lspexchn2 ⊢ φ → ¬ Y ∈ N ⁡ Z X

Proof

Step Hyp Ref Expression
1 lspexchn2.v ⊢ V = Base W
2 lspexchn2.n ⊢ N = LSpan ⁡ W
3 lspexchn2.w ⊢ φ → W ∈ LVec
4 lspexchn2.x ⊢ φ → X ∈ V
5 lspexchn2.y ⊢ φ → Y ∈ V
6 lspexchn2.z ⊢ φ → Z ∈ V
7 lspexchn2.q ⊢ φ → ¬ Y ∈ N ⁡ Z
8 lspexchn2.e ⊢ φ → ¬ X ∈ N ⁡ Z Y
9 prcom ⊢ Z Y = Y Z
10 9 fveq2i ⊢ N ⁡ Z Y = N ⁡ Y Z
11 10 eleq2i ⊢ X ∈ N ⁡ Z Y ↔ X ∈ N ⁡ Y Z
12 8 11 sylnib ⊢ φ → ¬ X ∈ N ⁡ Y Z
13 1 2 3 4 5 6 7 12 lspexchn1 ⊢ φ → ¬ Y ∈ N ⁡ X Z
14 prcom ⊢ X Z = Z X
15 14 fveq2i ⊢ N ⁡ X Z = N ⁡ Z X
16 15 eleq2i ⊢ Y ∈ N ⁡ X Z ↔ Y ∈ N ⁡ Z X
17 13 16 sylnib ⊢ φ → ¬ Y ∈ N ⁡ Z X