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