| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | otthg 5490 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑐 ∈ 𝑉) → (〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉 ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑))) | 
| 2 | 1 | 3expa 1119 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉 ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑))) | 
| 3 |  | simp3 1139 | . . . . . . . . . . 11
⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑) → 𝑐 = 𝑑) | 
| 4 | 2, 3 | biimtrdi 253 | . . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉 → 𝑐 = 𝑑)) | 
| 5 | 4 | con3rr3 155 | . . . . . . . . 9
⊢ (¬
𝑐 = 𝑑 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → ¬ 〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉)) | 
| 6 | 5 | imp 406 | . . . . . . . 8
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → ¬ 〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉) | 
| 7 | 6 | neqned 2947 | . . . . . . 7
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → 〈𝐴, 𝐵, 𝑐〉 ≠ 〈𝐴, 𝐵, 𝑑〉) | 
| 8 |  | disjsn2 4712 | . . . . . . 7
⊢
(〈𝐴, 𝐵, 𝑐〉 ≠ 〈𝐴, 𝐵, 𝑑〉 → ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅) | 
| 9 | 7, 8 | syl 17 | . . . . . 6
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅) | 
| 10 | 9 | expcom 413 | . . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (¬ 𝑐 = 𝑑 → ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) | 
| 11 | 10 | orrd 864 | . . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) | 
| 12 | 11 | adantrr 717 | . . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) | 
| 13 | 12 | ralrimivva 3202 | . 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) | 
| 14 |  | oteq3 4884 | . . . 4
⊢ (𝑐 = 𝑑 → 〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉) | 
| 15 | 14 | sneqd 4638 | . . 3
⊢ (𝑐 = 𝑑 → {〈𝐴, 𝐵, 𝑐〉} = {〈𝐴, 𝐵, 𝑑〉}) | 
| 16 | 15 | disjor 5125 | . 2
⊢
(Disj 𝑐
∈ 𝑉 {〈𝐴, 𝐵, 𝑐〉} ↔ ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) | 
| 17 | 13, 16 | sylibr 234 | 1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑉 {〈𝐴, 𝐵, 𝑐〉}) |