Step | Hyp | Ref
| Expression |
1 | | xpsc 16040 |
. . . 4
⊢ ◡({𝐴} +𝑐 {𝐵}) = (({∅} × {𝐴}) ∪ ({1𝑜} ×
{𝐵})) |
2 | 1 | fveq1i 6104 |
. . 3
⊢ (◡({𝐴} +𝑐 {𝐵})‘∅) = ((({∅} ×
{𝐴}) ∪
({1𝑜} × {𝐵}))‘∅) |
3 | | fnconstg 6006 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ({∅} × {𝐴}) Fn
{∅}) |
4 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
5 | | fvi 6165 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V → ( I
‘𝑥) = 𝑥) |
6 | 4, 5 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ( I
‘𝑥) = 𝑥 |
7 | | elsni 4142 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝐵} → ( I ‘𝑥) = ( I ‘𝐵)) |
9 | 6, 8 | syl5eqr 2658 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐵} → 𝑥 = ( I ‘𝐵)) |
10 | | velsn 4141 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {( I ‘𝐵)} ↔ 𝑥 = ( I ‘𝐵)) |
11 | 9, 10 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐵} → 𝑥 ∈ {( I ‘𝐵)}) |
12 | 11 | ssriv 3572 |
. . . . . . . . 9
⊢ {𝐵} ⊆ {( I ‘𝐵)} |
13 | | xpss2 5152 |
. . . . . . . . 9
⊢ ({𝐵} ⊆ {( I ‘𝐵)} →
({1𝑜} × {𝐵}) ⊆ ({1𝑜} ×
{( I ‘𝐵)})) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢
({1𝑜} × {𝐵}) ⊆ ({1𝑜} ×
{( I ‘𝐵)}) |
15 | | 1on 7454 |
. . . . . . . . . 10
⊢
1𝑜 ∈ On |
16 | 15 | elexi 3186 |
. . . . . . . . 9
⊢
1𝑜 ∈ V |
17 | | fvex 6113 |
. . . . . . . . 9
⊢ ( I
‘𝐵) ∈
V |
18 | 16, 17 | xpsn 6313 |
. . . . . . . 8
⊢
({1𝑜} × {( I ‘𝐵)}) = {〈1𝑜, ( I
‘𝐵)〉} |
19 | 14, 18 | sseqtri 3600 |
. . . . . . 7
⊢
({1𝑜} × {𝐵}) ⊆ {〈1𝑜, ( I
‘𝐵)〉} |
20 | 16, 17 | funsn 5853 |
. . . . . . 7
⊢ Fun
{〈1𝑜, ( I ‘𝐵)〉} |
21 | | funss 5822 |
. . . . . . 7
⊢
(({1𝑜} × {𝐵}) ⊆ {〈1𝑜, ( I
‘𝐵)〉} →
(Fun {〈1𝑜, ( I ‘𝐵)〉} → Fun ({1𝑜}
× {𝐵}))) |
22 | 19, 20, 21 | mp2 9 |
. . . . . 6
⊢ Fun
({1𝑜} × {𝐵}) |
23 | | funfn 5833 |
. . . . . 6
⊢ (Fun
({1𝑜} × {𝐵}) ↔ ({1𝑜} ×
{𝐵}) Fn dom
({1𝑜} × {𝐵})) |
24 | 22, 23 | mpbi 219 |
. . . . 5
⊢
({1𝑜} × {𝐵}) Fn dom ({1𝑜} ×
{𝐵}) |
25 | 24 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ({1𝑜} ×
{𝐵}) Fn dom
({1𝑜} × {𝐵})) |
26 | | dmxpss 5484 |
. . . . . . 7
⊢ dom
({1𝑜} × {𝐵}) ⊆
{1𝑜} |
27 | | sslin 3801 |
. . . . . . 7
⊢ (dom
({1𝑜} × {𝐵}) ⊆ {1𝑜} →
({∅} ∩ dom ({1𝑜} × {𝐵})) ⊆ ({∅} ∩
{1𝑜})) |
28 | 26, 27 | ax-mp 5 |
. . . . . 6
⊢
({∅} ∩ dom ({1𝑜} × {𝐵})) ⊆ ({∅} ∩
{1𝑜}) |
29 | | 1n0 7462 |
. . . . . . . 8
⊢
1𝑜 ≠ ∅ |
30 | 29 | necomi 2836 |
. . . . . . 7
⊢ ∅
≠ 1𝑜 |
31 | | disjsn2 4193 |
. . . . . . 7
⊢ (∅
≠ 1𝑜 → ({∅} ∩ {1𝑜}) =
∅) |
32 | 30, 31 | ax-mp 5 |
. . . . . 6
⊢
({∅} ∩ {1𝑜}) = ∅ |
33 | | sseq0 3927 |
. . . . . 6
⊢
((({∅} ∩ dom ({1𝑜} × {𝐵})) ⊆ ({∅} ∩
{1𝑜}) ∧ ({∅} ∩ {1𝑜}) =
∅) → ({∅} ∩ dom ({1𝑜} × {𝐵})) = ∅) |
34 | 28, 32, 33 | mp2an 704 |
. . . . 5
⊢
({∅} ∩ dom ({1𝑜} × {𝐵})) = ∅ |
35 | 34 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ({∅} ∩ dom
({1𝑜} × {𝐵})) = ∅) |
36 | | 0ex 4718 |
. . . . . 6
⊢ ∅
∈ V |
37 | 36 | snid 4155 |
. . . . 5
⊢ ∅
∈ {∅} |
38 | 37 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∅ ∈
{∅}) |
39 | | fvun1 6179 |
. . . 4
⊢
((({∅} × {𝐴}) Fn {∅} ∧
({1𝑜} × {𝐵}) Fn dom ({1𝑜} ×
{𝐵}) ∧ (({∅}
∩ dom ({1𝑜} × {𝐵})) = ∅ ∧ ∅ ∈
{∅})) → ((({∅} × {𝐴}) ∪ ({1𝑜} ×
{𝐵}))‘∅) =
(({∅} × {𝐴})‘∅)) |
40 | 3, 25, 35, 38, 39 | syl112anc 1322 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ((({∅} × {𝐴}) ∪
({1𝑜} × {𝐵}))‘∅) = (({∅} ×
{𝐴})‘∅)) |
41 | 2, 40 | syl5eq 2656 |
. 2
⊢ (𝐴 ∈ 𝑉 → (◡({𝐴} +𝑐 {𝐵})‘∅) = (({∅} ×
{𝐴})‘∅)) |
42 | | xpsng 6312 |
. . . . 5
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ({∅}
× {𝐴}) =
{〈∅, 𝐴〉}) |
43 | 42 | fveq1d 6105 |
. . . 4
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → (({∅}
× {𝐴})‘∅)
= ({〈∅, 𝐴〉}‘∅)) |
44 | | fvsng 6352 |
. . . 4
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → ({〈∅,
𝐴〉}‘∅) =
𝐴) |
45 | 43, 44 | eqtrd 2644 |
. . 3
⊢ ((∅
∈ V ∧ 𝐴 ∈
𝑉) → (({∅}
× {𝐴})‘∅)
= 𝐴) |
46 | 36, 45 | mpan 702 |
. 2
⊢ (𝐴 ∈ 𝑉 → (({∅} × {𝐴})‘∅) = 𝐴) |
47 | 41, 46 | eqtrd 2644 |
1
⊢ (𝐴 ∈ 𝑉 → (◡({𝐴} +𝑐 {𝐵})‘∅) = 𝐴) |