Step | Hyp | Ref
| Expression |
1 | | setscomd.ab |
. 2
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
2 | | setscomd.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑍) |
3 | | simpr 110 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → 𝑏 = 𝐵) |
4 | 3 | neeq2d 2376 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → (𝐴 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵)) |
5 | 3 | opeq1d 3796 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → ⟨𝑏, 𝐷⟩ = ⟨𝐵, 𝐷⟩) |
6 | 5 | oveq2d 5904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝑏, 𝐷⟩) = ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩)) |
7 | 5 | oveq2d 5904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → (𝑆 sSet ⟨𝑏, 𝐷⟩) = (𝑆 sSet ⟨𝐵, 𝐷⟩)) |
8 | 7 | oveq1d 5903 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 = 𝐵) → ((𝑆 sSet ⟨𝑏, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩)) |
9 | 6, 8 | eqeq12d 2202 |
. . . 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 2375 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → (𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝑏)) |
14 | 12 | opeq1d 3796 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ⟨𝑎, 𝐶⟩ = ⟨𝐴, 𝐶⟩) |
15 | 14 | oveq2d 5904 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → (𝑆 sSet ⟨𝑎, 𝐶⟩) = (𝑆 sSet ⟨𝐴, 𝐶⟩)) |
16 | 15 | oveq1d 5903 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ((𝑆 sSet ⟨𝑎, 𝐶⟩) sSet ⟨𝑏, 𝐷⟩) = ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝑏, 𝐷⟩)) |
17 | 14 | oveq2d 5904 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ((𝑆 sSet ⟨𝑏, 𝐷⟩) sSet ⟨𝑎, 𝐶⟩) = ((𝑆 sSet ⟨𝑏, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩)) |
18 | 16, 17 | eqeq12d 2202 |
. . . . 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 2752 |
. . . . . . 7
⊢ 𝑎 ∈ V |
28 | | vex 2752 |
. . . . . . 7
⊢ 𝑏 ∈ V |
29 | 27, 28 | setscom 12515 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑎 ≠ 𝑏) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet ⟨𝑎, 𝐶⟩) sSet ⟨𝑏, 𝐷⟩) = ((𝑆 sSet ⟨𝑏, 𝐷⟩) sSet ⟨𝑎, 𝐶⟩)) |
30 | 21, 22, 24, 26, 29 | syl22anc 1249 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → ((𝑆 sSet ⟨𝑎, 𝐶⟩) sSet ⟨𝑏, 𝐷⟩) = ((𝑆 sSet ⟨𝑏, 𝐷⟩) sSet ⟨𝑎, 𝐶⟩)) |
31 | 30 | ex 115 |
. . . 4
⊢ (𝜑 → (𝑎 ≠ 𝑏 → ((𝑆 sSet ⟨𝑎, 𝐶⟩) sSet ⟨𝑏, 𝐷⟩) = ((𝑆 sSet ⟨𝑏, 𝐷⟩) sSet ⟨𝑎, 𝐶⟩))) |
32 | 11, 19, 31 | vtocld 2801 |
. . 3
⊢ (𝜑 → (𝐴 ≠ 𝑏 → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝑏, 𝐷⟩) = ((𝑆 sSet ⟨𝑏, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))) |
33 | 2, 10, 32 | vtocld 2801 |
. 2
⊢ (𝜑 → (𝐴 ≠ 𝐵 → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩))) |
34 | 1, 33 | mpd 13 |
1
⊢ (𝜑 → ((𝑆 sSet ⟨𝐴, 𝐶⟩) sSet ⟨𝐵, 𝐷⟩) = ((𝑆 sSet ⟨𝐵, 𝐷⟩) sSet ⟨𝐴, 𝐶⟩)) |