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 𝑐 ∈ 𝑉 { ⟨ 𝐴 , 𝐵 , 𝑐 ⟩ } )