Theorem otsndisj 5521

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

Assertion

Ref	Expression
otsndisj	⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑉 {⟨𝐴, 𝐵, 𝑐⟩})

Distinct variable groups:   𝐴,𝑐   𝐵,𝑐   𝑉,𝑐   𝑋,𝑐   𝑌,𝑐

Proof of Theorem otsndisj

Dummy variable 𝑑 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		otthg 5487	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑐 ∈ 𝑉) → (⟨𝐴, 𝐵, 𝑐⟩ = ⟨𝐴, 𝐵, 𝑑⟩ ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑)))
2	1	3expa 1116	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (⟨𝐴, 𝐵, 𝑐⟩ = ⟨𝐴, 𝐵, 𝑑⟩ ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑)))
3		simp3 1136	. . . . . . . . . . 11 ⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑) → 𝑐 = 𝑑)
4	2, 3	biimtrdi 252	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (⟨𝐴, 𝐵, 𝑐⟩ = ⟨𝐴, 𝐵, 𝑑⟩ → 𝑐 = 𝑑))
5	4	con3rr3 155	. . . . . . . . 9 ⊢ (¬ 𝑐 = 𝑑 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → ¬ ⟨𝐴, 𝐵, 𝑐⟩ = ⟨𝐴, 𝐵, 𝑑⟩))
6	5	imp 406	. . . . . . . 8 ⊢ ((¬ 𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → ¬ ⟨𝐴, 𝐵, 𝑐⟩ = ⟨𝐴, 𝐵, 𝑑⟩)
7	6	neqned 2944	. . . . . . 7 ⊢ ((¬ 𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → ⟨𝐴, 𝐵, 𝑐⟩ ≠ ⟨𝐴, 𝐵, 𝑑⟩)
8		disjsn2 4717	. . . . . . 7 ⊢ (⟨𝐴, 𝐵, 𝑐⟩ ≠ ⟨𝐴, 𝐵, 𝑑⟩ → ({⟨𝐴, 𝐵, 𝑐⟩} ∩ {⟨𝐴, 𝐵, 𝑑⟩}) = ∅)
9	7, 8	syl 17	. . . . . 6 ⊢ ((¬ 𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → ({⟨𝐴, 𝐵, 𝑐⟩} ∩ {⟨𝐴, 𝐵, 𝑑⟩}) = ∅)
10	9	expcom 413	. . . . 5 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (¬ 𝑐 = 𝑑 → ({⟨𝐴, 𝐵, 𝑐⟩} ∩ {⟨𝐴, 𝐵, 𝑑⟩}) = ∅))
11	10	orrd 862	. . . 4 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (𝑐 = 𝑑 ∨ ({⟨𝐴, 𝐵, 𝑐⟩} ∩ {⟨𝐴, 𝐵, 𝑑⟩}) = ∅))
12	11	adantrr 716	. . 3 ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑐 = 𝑑 ∨ ({⟨𝐴, 𝐵, 𝑐⟩} ∩ {⟨𝐴, 𝐵, 𝑑⟩}) = ∅))
13	12	ralrimivva 3197	. 2 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 = 𝑑 ∨ ({⟨𝐴, 𝐵, 𝑐⟩} ∩ {⟨𝐴, 𝐵, 𝑑⟩}) = ∅))
14		oteq3 4885	. . . 4 ⊢ (𝑐 = 𝑑 → ⟨𝐴, 𝐵, 𝑐⟩ = ⟨𝐴, 𝐵, 𝑑⟩)
15	14	sneqd 4641	. . 3 ⊢ (𝑐 = 𝑑 → {⟨𝐴, 𝐵, 𝑐⟩} = {⟨𝐴, 𝐵, 𝑑⟩})
16	15	disjor 5128	. 2 ⊢ (Disj 𝑐 ∈ 𝑉 {⟨𝐴, 𝐵, 𝑐⟩} ↔ ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 = 𝑑 ∨ ({⟨𝐴, 𝐵, 𝑐⟩} ∩ {⟨𝐴, 𝐵, 𝑑⟩}) = ∅))
17	13, 16	sylibr 233	1 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑉 {⟨𝐴, 𝐵, 𝑐⟩})

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 846   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   ≠ wne 2937  ∀wral 3058   ∩ cin 3946  ∅c0 4323  {csn 4629  ⟨cotp 4637  Disj wdisj 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-11 2147  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-mo 2530  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rmo 3373  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-ot 4638  df-disj 5114

This theorem is referenced by: (None)