Proof of Theorem setscom
Step | Hyp | Ref
| Expression |
1 | | rescom 4904 |
. . . . . 6
⊢ ((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) = ((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) |
2 | 1 | uneq1i 3268 |
. . . . 5
⊢ (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {〈𝐴, 𝐶〉}) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉}) |
3 | 2 | uneq1i 3268 |
. . . 4
⊢ ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {〈𝐴, 𝐶〉}) ∪ {〈𝐵, 𝐷〉}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉}) ∪ {〈𝐵, 𝐷〉}) |
4 | | un23 3277 |
. . . 4
⊢ ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉}) ∪ {〈𝐵, 𝐷〉}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐵, 𝐷〉}) ∪ {〈𝐴, 𝐶〉}) |
5 | 3, 4 | eqtri 2185 |
. . 3
⊢ ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {〈𝐴, 𝐶〉}) ∪ {〈𝐵, 𝐷〉}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐵, 𝐷〉}) ∪ {〈𝐴, 𝐶〉}) |
6 | | setscom.1 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
7 | | setsvala 12388 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ V ∧ 𝐶 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐶〉) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉})) |
8 | 6, 7 | mp3an2 1314 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐶〉) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉})) |
9 | 8 | ad2ant2r 501 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (𝑆 sSet 〈𝐴, 𝐶〉) = ((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉})) |
10 | 9 | reseq1d 4878 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐴, 𝐶〉) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉}) ↾ (V ∖ {𝐵}))) |
11 | | resundir 4893 |
. . . . . 6
⊢ (((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉}) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ ({〈𝐴, 𝐶〉} ↾ (V ∖ {𝐵}))) |
12 | | elex 2733 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝑊 → 𝐶 ∈ V) |
13 | 12 | ad2antrl 482 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 𝐶 ∈ V) |
14 | | opelxpi 4631 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → 〈𝐴, 𝐶〉 ∈ (V ×
V)) |
15 | 6, 13, 14 | sylancr 411 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 〈𝐴, 𝐶〉 ∈ (V ×
V)) |
16 | | opexg 4201 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → 〈𝐴, 𝐶〉 ∈ V) |
17 | 6, 13, 16 | sylancr 411 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 〈𝐴, 𝐶〉 ∈ V) |
18 | | relsng 4702 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐶〉 ∈ V → (Rel
{〈𝐴, 𝐶〉} ↔ 〈𝐴, 𝐶〉 ∈ (V ×
V))) |
19 | 17, 18 | syl 14 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (Rel {〈𝐴, 𝐶〉} ↔ 〈𝐴, 𝐶〉 ∈ (V ×
V))) |
20 | 15, 19 | mpbird 166 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → Rel {〈𝐴, 𝐶〉}) |
21 | | dmsnopg 5070 |
. . . . . . . . . 10
⊢ (𝐶 ∈ V → dom
{〈𝐴, 𝐶〉} = {𝐴}) |
22 | 13, 21 | syl 14 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → dom {〈𝐴, 𝐶〉} = {𝐴}) |
23 | | disjsn2 3634 |
. . . . . . . . . . 11
⊢ (𝐴 ≠ 𝐵 → ({𝐴} ∩ {𝐵}) = ∅) |
24 | 23 | ad2antlr 481 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ({𝐴} ∩ {𝐵}) = ∅) |
25 | | disj2 3460 |
. . . . . . . . . 10
⊢ (({𝐴} ∩ {𝐵}) = ∅ ↔ {𝐴} ⊆ (V ∖ {𝐵})) |
26 | 24, 25 | sylib 121 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → {𝐴} ⊆ (V ∖ {𝐵})) |
27 | 22, 26 | eqsstrd 3174 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → dom {〈𝐴, 𝐶〉} ⊆ (V ∖ {𝐵})) |
28 | | relssres 4917 |
. . . . . . . 8
⊢ ((Rel
{〈𝐴, 𝐶〉} ∧ dom {〈𝐴, 𝐶〉} ⊆ (V ∖ {𝐵})) → ({〈𝐴, 𝐶〉} ↾ (V ∖ {𝐵})) = {〈𝐴, 𝐶〉}) |
29 | 20, 27, 28 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ({〈𝐴, 𝐶〉} ↾ (V ∖ {𝐵})) = {〈𝐴, 𝐶〉}) |
30 | 29 | uneq2d 3272 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ ({〈𝐴, 𝐶〉} ↾ (V ∖ {𝐵}))) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {〈𝐴, 𝐶〉})) |
31 | 11, 30 | syl5eq 2209 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (((𝑆 ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉}) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {〈𝐴, 𝐶〉})) |
32 | 10, 31 | eqtrd 2197 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐴, 𝐶〉) ↾ (V ∖ {𝐵})) = (((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {〈𝐴, 𝐶〉})) |
33 | 32 | uneq1d 3271 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (((𝑆 sSet 〈𝐴, 𝐶〉) ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉}) = ((((𝑆 ↾ (V ∖ {𝐴})) ↾ (V ∖ {𝐵})) ∪ {〈𝐴, 𝐶〉}) ∪ {〈𝐵, 𝐷〉})) |
34 | | setscom.2 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
35 | | setsvala 12388 |
. . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ V ∧ 𝐷 ∈ 𝑋) → (𝑆 sSet 〈𝐵, 𝐷〉) = ((𝑆 ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉})) |
36 | 34, 35 | mp3an2 1314 |
. . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐷 ∈ 𝑋) → (𝑆 sSet 〈𝐵, 𝐷〉) = ((𝑆 ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉})) |
37 | 36 | reseq1d 4878 |
. . . . . 6
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐷 ∈ 𝑋) → ((𝑆 sSet 〈𝐵, 𝐷〉) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉}) ↾ (V ∖ {𝐴}))) |
38 | 37 | ad2ant2rl 503 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐵, 𝐷〉) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉}) ↾ (V ∖ {𝐴}))) |
39 | | resundir 4893 |
. . . . . 6
⊢ (((𝑆 ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐵, 𝐷〉} ↾ (V ∖ {𝐴}))) |
40 | | elex 2733 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ 𝑋 → 𝐷 ∈ V) |
41 | 40 | ad2antll 483 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 𝐷 ∈ V) |
42 | | opelxpi 4631 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ V ∧ 𝐷 ∈ V) → 〈𝐵, 𝐷〉 ∈ (V ×
V)) |
43 | 34, 41, 42 | sylancr 411 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 〈𝐵, 𝐷〉 ∈ (V ×
V)) |
44 | | opexg 4201 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ 𝐷 ∈ V) → 〈𝐵, 𝐷〉 ∈ V) |
45 | 34, 41, 44 | sylancr 411 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 〈𝐵, 𝐷〉 ∈ V) |
46 | | relsng 4702 |
. . . . . . . . . 10
⊢
(〈𝐵, 𝐷〉 ∈ V → (Rel
{〈𝐵, 𝐷〉} ↔ 〈𝐵, 𝐷〉 ∈ (V ×
V))) |
47 | 45, 46 | syl 14 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (Rel {〈𝐵, 𝐷〉} ↔ 〈𝐵, 𝐷〉 ∈ (V ×
V))) |
48 | 43, 47 | mpbird 166 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → Rel {〈𝐵, 𝐷〉}) |
49 | | dmsnopg 5070 |
. . . . . . . . . 10
⊢ (𝐷 ∈ V → dom
{〈𝐵, 𝐷〉} = {𝐵}) |
50 | 41, 49 | syl 14 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → dom {〈𝐵, 𝐷〉} = {𝐵}) |
51 | | ssv 3160 |
. . . . . . . . . . 11
⊢ {𝐴} ⊆ V |
52 | | ssv 3160 |
. . . . . . . . . . 11
⊢ {𝐵} ⊆ V |
53 | | ssconb 3251 |
. . . . . . . . . . 11
⊢ (({𝐴} ⊆ V ∧ {𝐵} ⊆ V) → ({𝐴} ⊆ (V ∖ {𝐵}) ↔ {𝐵} ⊆ (V ∖ {𝐴}))) |
54 | 51, 52, 53 | mp2an 423 |
. . . . . . . . . 10
⊢ ({𝐴} ⊆ (V ∖ {𝐵}) ↔ {𝐵} ⊆ (V ∖ {𝐴})) |
55 | 26, 54 | sylib 121 |
. . . . . . . . 9
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → {𝐵} ⊆ (V ∖ {𝐴})) |
56 | 50, 55 | eqsstrd 3174 |
. . . . . . . 8
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → dom {〈𝐵, 𝐷〉} ⊆ (V ∖ {𝐴})) |
57 | | relssres 4917 |
. . . . . . . 8
⊢ ((Rel
{〈𝐵, 𝐷〉} ∧ dom {〈𝐵, 𝐷〉} ⊆ (V ∖ {𝐴})) → ({〈𝐵, 𝐷〉} ↾ (V ∖ {𝐴})) = {〈𝐵, 𝐷〉}) |
58 | 48, 56, 57 | syl2anc 409 |
. . . . . . 7
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ({〈𝐵, 𝐷〉} ↾ (V ∖ {𝐴})) = {〈𝐵, 𝐷〉}) |
59 | 58 | uneq2d 3272 |
. . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ ({〈𝐵, 𝐷〉} ↾ (V ∖ {𝐴}))) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐵, 𝐷〉})) |
60 | 39, 59 | syl5eq 2209 |
. . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (((𝑆 ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉}) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐵, 𝐷〉})) |
61 | 38, 60 | eqtrd 2197 |
. . . 4
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐵, 𝐷〉) ↾ (V ∖ {𝐴})) = (((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐵, 𝐷〉})) |
62 | 61 | uneq1d 3271 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (((𝑆 sSet 〈𝐵, 𝐷〉) ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉}) = ((((𝑆 ↾ (V ∖ {𝐵})) ↾ (V ∖ {𝐴})) ∪ {〈𝐵, 𝐷〉}) ∪ {〈𝐴, 𝐶〉})) |
63 | 5, 33, 62 | 3eqtr4a 2223 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (((𝑆 sSet 〈𝐴, 𝐶〉) ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉}) = (((𝑆 sSet 〈𝐵, 𝐷〉) ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉})) |
64 | | setsex 12389 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐴 ∈ V ∧ 𝐶 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐶〉) ∈ V) |
65 | 6, 64 | mp3an2 1314 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊) → (𝑆 sSet 〈𝐴, 𝐶〉) ∈ V) |
66 | 65 | ad2ant2r 501 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (𝑆 sSet 〈𝐴, 𝐶〉) ∈ V) |
67 | 34 | a1i 9 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 𝐵 ∈ V) |
68 | | simprr 522 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 𝐷 ∈ 𝑋) |
69 | | setsvala 12388 |
. . 3
⊢ (((𝑆 sSet 〈𝐴, 𝐶〉) ∈ V ∧ 𝐵 ∈ V ∧ 𝐷 ∈ 𝑋) → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = (((𝑆 sSet 〈𝐴, 𝐶〉) ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉})) |
70 | 66, 67, 68, 69 | syl3anc 1227 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = (((𝑆 sSet 〈𝐴, 𝐶〉) ↾ (V ∖ {𝐵})) ∪ {〈𝐵, 𝐷〉})) |
71 | | setsex 12389 |
. . . . 5
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐵 ∈ V ∧ 𝐷 ∈ 𝑋) → (𝑆 sSet 〈𝐵, 𝐷〉) ∈ V) |
72 | 34, 71 | mp3an2 1314 |
. . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐷 ∈ 𝑋) → (𝑆 sSet 〈𝐵, 𝐷〉) ∈ V) |
73 | 72 | ad2ant2rl 503 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → (𝑆 sSet 〈𝐵, 𝐷〉) ∈ V) |
74 | 6 | a1i 9 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 𝐴 ∈ V) |
75 | | simprl 521 |
. . 3
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → 𝐶 ∈ 𝑊) |
76 | | setsvala 12388 |
. . 3
⊢ (((𝑆 sSet 〈𝐵, 𝐷〉) ∈ V ∧ 𝐴 ∈ V ∧ 𝐶 ∈ 𝑊) → ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉) = (((𝑆 sSet 〈𝐵, 𝐷〉) ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉})) |
77 | 73, 74, 75, 76 | syl3anc 1227 |
. 2
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉) = (((𝑆 sSet 〈𝐵, 𝐷〉) ↾ (V ∖ {𝐴})) ∪ {〈𝐴, 𝐶〉})) |
78 | 63, 70, 77 | 3eqtr4d 2207 |
1
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) ∧ (𝐶 ∈ 𝑊 ∧ 𝐷 ∈ 𝑋)) → ((𝑆 sSet 〈𝐴, 𝐶〉) sSet 〈𝐵, 𝐷〉) = ((𝑆 sSet 〈𝐵, 𝐷〉) sSet 〈𝐴, 𝐶〉)) |