Step | Hyp | Ref
| Expression |
1 | | otthg 5399 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑐 ∈ 𝑉) → (〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉 ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑))) |
2 | 1 | 3expa 1117 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉 ↔ (𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑))) |
3 | | simp3 1137 |
. . . . . . . . . . 11
⊢ ((𝐴 = 𝐴 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑑) → 𝑐 = 𝑑) |
4 | 2, 3 | syl6bi 252 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉 → 𝑐 = 𝑑)) |
5 | 4 | con3rr3 155 |
. . . . . . . . 9
⊢ (¬
𝑐 = 𝑑 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → ¬ 〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉)) |
6 | 5 | imp 407 |
. . . . . . . 8
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → ¬ 〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉) |
7 | 6 | neqned 2950 |
. . . . . . 7
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → 〈𝐴, 𝐵, 𝑐〉 ≠ 〈𝐴, 𝐵, 𝑑〉) |
8 | | disjsn2 4649 |
. . . . . . 7
⊢
(〈𝐴, 𝐵, 𝑐〉 ≠ 〈𝐴, 𝐵, 𝑑〉 → ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅) |
9 | 7, 8 | syl 17 |
. . . . . 6
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉)) → ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅) |
10 | 9 | expcom 414 |
. . . . 5
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (¬ 𝑐 = 𝑑 → ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) |
11 | 10 | orrd 860 |
. . . 4
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ 𝑐 ∈ 𝑉) → (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) |
12 | 11 | adantrr 714 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) |
13 | 12 | ralrimivva 3120 |
. 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) |
14 | | oteq3 4816 |
. . . 4
⊢ (𝑐 = 𝑑 → 〈𝐴, 𝐵, 𝑐〉 = 〈𝐴, 𝐵, 𝑑〉) |
15 | 14 | sneqd 4574 |
. . 3
⊢ (𝑐 = 𝑑 → {〈𝐴, 𝐵, 𝑐〉} = {〈𝐴, 𝐵, 𝑑〉}) |
16 | 15 | disjor 5054 |
. 2
⊢
(Disj 𝑐
∈ 𝑉 {〈𝐴, 𝐵, 𝑐〉} ↔ ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 = 𝑑 ∨ ({〈𝐴, 𝐵, 𝑐〉} ∩ {〈𝐴, 𝐵, 𝑑〉}) = ∅)) |
17 | 13, 16 | sylibr 233 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑉 {〈𝐴, 𝐵, 𝑐〉}) |