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

Metamath Proof Explorer

Theorem otsndisj

Description: The singletons consisting of ordered triples which have distinct third components are disjoint. (Contributed by Alexander van der Vekens, 10-Mar-2018)

Ref Expression
Assertion otsndisj ⊢ A ∈ X ∧ B ∈ Y → Disj c ∈ V A B c

Proof

Step Hyp Ref Expression
1 otthg ⊢ A ∈ X ∧ B ∈ Y ∧ c ∈ V → A B c = A B d ↔ A = A ∧ B = B ∧ c = d
2 1 3expa ⊢ A ∈ X ∧ B ∈ Y ∧ c ∈ V → A B c = A B d ↔ A = A ∧ B = B ∧ c = d
3 simp3 ⊢ A = A ∧ B = B ∧ c = d → c = d
4 2 3 biimtrdi ⊢ A ∈ X ∧ B ∈ Y ∧ c ∈ V → A B c = A B d → c = d
5 4 con3rr3 ⊢ ¬ c = d → A ∈ X ∧ B ∈ Y ∧ c ∈ V → ¬ A B c = A B d
6 5 imp ⊢ ¬ c = d ∧ A ∈ X ∧ B ∈ Y ∧ c ∈ V → ¬ A B c = A B d
7 6 neqned ⊢ ¬ c = d ∧ A ∈ X ∧ B ∈ Y ∧ c ∈ V → A B c ≠ A B d
8 disjsn2 ⊢ A B c ≠ A B d → A B c ∩ A B d = ∅
9 7 8 syl ⊢ ¬ c = d ∧ A ∈ X ∧ B ∈ Y ∧ c ∈ V → A B c ∩ A B d = ∅
10 9 expcom ⊢ A ∈ X ∧ B ∈ Y ∧ c ∈ V → ¬ c = d → A B c ∩ A B d = ∅
11 10 orrd ⊢ A ∈ X ∧ B ∈ Y ∧ c ∈ V → c = d ∨ A B c ∩ A B d = ∅
12 11 adantrr ⊢ A ∈ X ∧ B ∈ Y ∧ c ∈ V ∧ d ∈ V → c = d ∨ A B c ∩ A B d = ∅
13 12 ralrimivva ⊢ A ∈ X ∧ B ∈ Y → ∀ c ∈ V ∀ d ∈ V c = d ∨ A B c ∩ A B d = ∅
14 oteq3 ⊢ c = d → A B c = A B d
15 14 sneqd ⊢ c = d → A B c = A B d
16 15 disjor ⊢ Disj c ∈ V A B c ↔ ∀ c ∈ V ∀ d ∈ V c = d ∨ A B c ∩ A B d = ∅
17 13 16 sylibr ⊢ A ∈ X ∧ B ∈ Y → Disj c ∈ V A B c