Step | Hyp | Ref
| Expression |
1 | | xpsc 16603 |
. . . 4
⊢ ◡({𝐴} +𝑐 {𝐵}) = (({∅} × {𝐴}) ∪ ({1o} × {𝐵})) |
2 | 1 | fveq1i 6447 |
. . 3
⊢ (◡({𝐴} +𝑐 {𝐵})‘∅) = ((({∅} ×
{𝐴}) ∪ ({1o}
× {𝐵}))‘∅) |
3 | | fnconstg 6343 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ({∅} × {𝐴}) Fn
{∅}) |
4 | | fvi 6515 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V → ( I
‘𝑥) = 𝑥) |
5 | 4 | elv 3402 |
. . . . . . . . . . . 12
⊢ ( I
‘𝑥) = 𝑥 |
6 | | elsni 4415 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) |
7 | 6 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝐵} → ( I ‘𝑥) = ( I ‘𝐵)) |
8 | 5, 7 | syl5eqr 2828 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐵} → 𝑥 = ( I ‘𝐵)) |
9 | | velsn 4414 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {( I ‘𝐵)} ↔ 𝑥 = ( I ‘𝐵)) |
10 | 8, 9 | sylibr 226 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐵} → 𝑥 ∈ {( I ‘𝐵)}) |
11 | 10 | ssriv 3825 |
. . . . . . . . 9
⊢ {𝐵} ⊆ {( I ‘𝐵)} |
12 | | xpss2 5375 |
. . . . . . . . 9
⊢ ({𝐵} ⊆ {( I ‘𝐵)} → ({1o}
× {𝐵}) ⊆
({1o} × {( I ‘𝐵)})) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
⊢
({1o} × {𝐵}) ⊆ ({1o} × {( I
‘𝐵)}) |
14 | | 1oex 7851 |
. . . . . . . . 9
⊢
1o ∈ V |
15 | | fvex 6459 |
. . . . . . . . 9
⊢ ( I
‘𝐵) ∈
V |
16 | 14, 15 | xpsn 6672 |
. . . . . . . 8
⊢
({1o} × {( I ‘𝐵)}) = {〈1o, ( I ‘𝐵)〉} |
17 | 13, 16 | sseqtri 3856 |
. . . . . . 7
⊢
({1o} × {𝐵}) ⊆ {〈1o, ( I
‘𝐵)〉} |
18 | 14, 15 | funsn 6187 |
. . . . . . 7
⊢ Fun
{〈1o, ( I ‘𝐵)〉} |
19 | | funss 6154 |
. . . . . . 7
⊢
(({1o} × {𝐵}) ⊆ {〈1o, ( I
‘𝐵)〉} →
(Fun {〈1o, ( I ‘𝐵)〉} → Fun ({1o} ×
{𝐵}))) |
20 | 17, 18, 19 | mp2 9 |
. . . . . 6
⊢ Fun
({1o} × {𝐵}) |
21 | | funfn 6165 |
. . . . . 6
⊢ (Fun
({1o} × {𝐵}) ↔ ({1o} × {𝐵}) Fn dom ({1o}
× {𝐵})) |
22 | 20, 21 | mpbi 222 |
. . . . 5
⊢
({1o} × {𝐵}) Fn dom ({1o} × {𝐵}) |
23 | 22 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ({1o} × {𝐵}) Fn dom ({1o}
× {𝐵})) |
24 | | dmxpss 5819 |
. . . . . . 7
⊢ dom
({1o} × {𝐵}) ⊆ {1o} |
25 | | sslin 4059 |
. . . . . . 7
⊢ (dom
({1o} × {𝐵}) ⊆ {1o} → ({∅}
∩ dom ({1o} × {𝐵})) ⊆ ({∅} ∩
{1o})) |
26 | 24, 25 | ax-mp 5 |
. . . . . 6
⊢
({∅} ∩ dom ({1o} × {𝐵})) ⊆ ({∅} ∩
{1o}) |
27 | | 1n0 7859 |
. . . . . . . 8
⊢
1o ≠ ∅ |
28 | 27 | necomi 3023 |
. . . . . . 7
⊢ ∅
≠ 1o |
29 | | disjsn2 4479 |
. . . . . . 7
⊢ (∅
≠ 1o → ({∅} ∩ {1o}) =
∅) |
30 | 28, 29 | ax-mp 5 |
. . . . . 6
⊢
({∅} ∩ {1o}) = ∅ |
31 | | sseq0 4201 |
. . . . . 6
⊢
((({∅} ∩ dom ({1o} × {𝐵})) ⊆ ({∅} ∩
{1o}) ∧ ({∅} ∩ {1o}) = ∅) →
({∅} ∩ dom ({1o} × {𝐵})) = ∅) |
32 | 26, 30, 31 | mp2an 682 |
. . . . 5
⊢
({∅} ∩ dom ({1o} × {𝐵})) = ∅ |
33 | 32 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ({∅} ∩ dom
({1o} × {𝐵})) = ∅) |
34 | | 0ex 5026 |
. . . . . 6
⊢ ∅
∈ V |
35 | 34 | snid 4430 |
. . . . 5
⊢ ∅
∈ {∅} |
36 | 35 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∅ ∈
{∅}) |
37 | | fvun1 6529 |
. . . 4
⊢
((({∅} × {𝐴}) Fn {∅} ∧ ({1o}
× {𝐵}) Fn dom
({1o} × {𝐵}) ∧ (({∅} ∩ dom
({1o} × {𝐵})) = ∅ ∧ ∅ ∈
{∅})) → ((({∅} × {𝐴}) ∪ ({1o} × {𝐵}))‘∅) = (({∅}
× {𝐴})‘∅)) |
38 | 3, 23, 33, 36, 37 | syl112anc 1442 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((({∅} × {𝐴}) ∪ ({1o}
× {𝐵}))‘∅) = (({∅} ×
{𝐴})‘∅)) |
39 | 2, 38 | syl5eq 2826 |
. 2
⊢ (𝐴 ∈ 𝑉 → (◡({𝐴} +𝑐 {𝐵})‘∅) = (({∅} ×
{𝐴})‘∅)) |
40 | | xpsng 6671 |
. . . . 5
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ({∅}
× {𝐴}) =
{〈∅, 𝐴〉}) |
41 | 40 | fveq1d 6448 |
. . . 4
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → (({∅}
× {𝐴})‘∅)
= ({〈∅, 𝐴〉}‘∅)) |
42 | | fvsng 6713 |
. . . 4
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ({〈∅,
𝐴〉}‘∅) =
𝐴) |
43 | 41, 42 | eqtrd 2814 |
. . 3
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → (({∅}
× {𝐴})‘∅)
= 𝐴) |
44 | 34, 43 | mpan 680 |
. 2
⊢ (𝐴 ∈ 𝑉 → (({∅} × {𝐴})‘∅) = 𝐴) |
45 | 39, 44 | eqtrd 2814 |
1
⊢ (𝐴 ∈ 𝑉 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |