Step | Hyp | Ref
| Expression |
1 | | setscomd.ab |
. 2
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
2 | | setscomd.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑍) |
3 | | simpr 110 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
4 | 3 | neeq2d 2366 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → (𝐴 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵)) |
5 | 3 | opeq1d 3786 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → 〈𝑏, 𝐷〉 = 〈𝐵, 𝐷〉) |
6 | 5 | oveq2d 5893 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉)) |
7 | 5 | oveq2d 5893 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → (𝑆 sSet 〈𝑏, 𝐷〉) = (𝑆 sSet 〈𝐵, 𝐷〉)) |
8 | 7 | oveq1d 5892 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝐴, 𝐶〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)) |
9 | 6, 8 | eqeq12d 2192 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → (((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝐴, 𝐶〉) ↔ ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉))) |
10 | 4, 9 | imbi12d 234 |
. . 3
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → ((𝐴 ≠ 𝑏 → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝐴, 𝐶〉)) ↔ (𝐴 ≠ 𝐵 → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)))) |
11 | | setscomd.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑌) |
12 | | simpr 110 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → 𝑎 = 𝐴) |
13 | 12 | neeq1d 2365 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → (𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝑏)) |
14 | 12 | opeq1d 3786 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → 〈𝑎, 𝐶〉 = 〈𝐴, 𝐶〉) |
15 | 14 | oveq2d 5893 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → (𝑆 sSet 〈𝑎, 𝐶〉) = (𝑆 sSet 〈𝐴, 𝐶〉)) |
16 | 15 | oveq1d 5892 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ((𝑆 sSet 〈𝑎, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝑏, 𝐷〉)) |
17 | 14 | oveq2d 5893 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝑎, 𝐶〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝐴, 𝐶〉)) |
18 | 16, 17 | eqeq12d 2192 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → (((𝑆 sSet 〈𝑎, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝑎, 𝐶〉) ↔ ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝐴, 𝐶〉))) |
19 | 13, 18 | imbi12d 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ((𝑎 ≠ 𝑏 → ((𝑆 sSet 〈𝑎, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝑎, 𝐶〉)) ↔ (𝐴 ≠ 𝑏 → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝐴, 𝐶〉)))) |
20 | | setscomd.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
21 | 20 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → 𝑆 ∈ 𝑉) |
22 | | simpr 110 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → 𝑎 ≠ 𝑏) |
23 | | setscomd.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑊) |
24 | 23 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → 𝐶 ∈ 𝑊) |
25 | | setscomd.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑋) |
26 | 25 | adantr 276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → 𝐷 ∈ 𝑋) |
27 | | vex 2742 |
. . . . . . 7
⊢ 𝑎 ∈ V |
28 | | vex 2742 |
. . . . . . 7
⊢ 𝑏 ∈ V |
29 | 27, 28 | setscom 12504 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝑎, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝑎, 𝐶〉)) |
30 | 21, 22, 24, 26, 29 | syl22anc 1239 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → ((𝑆 sSet 〈𝑎, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝑎, 𝐶〉)) |
31 | 30 | ex 115 |
. . . 4
⊢ (𝜑 → (𝑎 ≠ 𝑏 → ((𝑆 sSet 〈𝑎, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝑎, 𝐶〉))) |
32 | 11, 19, 31 | vtocld 2791 |
. . 3
⊢ (𝜑 → (𝐴 ≠ 𝑏 → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝑏, 𝐷〉) = ((𝑆 sSet 〈𝑏, 𝐷〉) sSet 〈𝐴, 𝐶〉))) |
33 | 2, 10, 32 | vtocld 2791 |
. 2
⊢ (𝜑 → (𝐴 ≠ 𝐵 → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉))) |
34 | 1, 33 | mpd 13 |
1
⊢ (𝜑 → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)) |