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 ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → Disj 𝑐 ∈ 𝑉 { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } )

Proof

Step Hyp Ref Expression
1 otthg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑐 ∈ 𝑉 ) → ( ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ ↔ ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑 ) ) )
2 1 3expa ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) → ( ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ ↔ ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑 ) ) )
3 simp3 ⊢ ( ( 𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑 ) → 𝑐 = 𝑑 )
4 2 3 biimtrdi ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) → ( ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ → 𝑐 = 𝑑 ) )
5 4 con3rr3 ⊢ ( ¬ 𝑐 = 𝑑 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) → ¬ ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ ) )
6 5 imp ⊢ ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) ) → ¬ ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ )
7 6 neqned ⊢ ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) ) → ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ ≠ ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ )
8 disjsn2 ⊢ ( ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ ≠ ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ → ( { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ∩ { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } ) = ∅ )
9 7 8 syl ⊢ ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) ) → ( { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ∩ { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } ) = ∅ )
10 9 expcom ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) → ( ¬ 𝑐 = 𝑑 → ( { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ∩ { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } ) = ∅ ) )
11 10 orrd ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑐 ∈ 𝑉 ) → ( 𝑐 = 𝑑 ∨ ( { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ∩ { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } ) = ∅ ) )
12 11 adantrr ⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑐 = 𝑑 ∨ ( { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ∩ { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } ) = ∅ ) )
13 12 ralrimivva ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ∀ 𝑐 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ( 𝑐 = 𝑑 ∨ ( { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ∩ { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } ) = ∅ ) )
14 oteq3 ⊢ ( 𝑐 = 𝑑 → ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ = ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ )
15 14 sneqd ⊢ ( 𝑐 = 𝑑 → { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } = { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } )
16 15 disjor ⊢ ( Disj 𝑐 ∈ 𝑉 { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ↔ ∀ 𝑐 ∈ 𝑉 ∀ 𝑑 ∈ 𝑉 ( 𝑐 = 𝑑 ∨ ( { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } ∩ { ⟨ 𝐴 , 𝐵 , 𝑑 ⟩ } ) = ∅ ) )
17 13 16 sylibr ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → Disj 𝑐 ∈ 𝑉 { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } )