Proof of Theorem xpsfrnel2
Step | Hyp | Ref
| Expression |
1 | | xpsfrnel 16046 |
. 2
⊢ (◡({𝑋} +𝑐 {𝑌}) ∈ X𝑘 ∈ 2𝑜
if(𝑘 = ∅, 𝐴, 𝐵) ↔ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵)) |
2 | | 0ex 4718 |
. . . . . . . . . 10
⊢ ∅
∈ V |
3 | 2 | prid1 4241 |
. . . . . . . . 9
⊢ ∅
∈ {∅, 1𝑜} |
4 | | df2o3 7460 |
. . . . . . . . 9
⊢
2𝑜 = {∅,
1𝑜} |
5 | 3, 4 | eleqtrri 2687 |
. . . . . . . 8
⊢ ∅
∈ 2𝑜 |
6 | | fndm 5904 |
. . . . . . . 8
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → dom ◡({𝑋} +𝑐 {𝑌}) = 2𝑜) |
7 | 5, 6 | syl5eleqr 2695 |
. . . . . . 7
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → ∅
∈ dom ◡({𝑋} +𝑐 {𝑌})) |
8 | | xpsc 16040 |
. . . . . . . . 9
⊢ ◡({𝑋} +𝑐 {𝑌}) = (({∅} × {𝑋}) ∪ ({1𝑜} ×
{𝑌})) |
9 | 8 | dmeqi 5247 |
. . . . . . . 8
⊢ dom ◡({𝑋} +𝑐 {𝑌}) = dom (({∅} × {𝑋}) ∪
({1𝑜} × {𝑌})) |
10 | | dmun 5253 |
. . . . . . . 8
⊢ dom
(({∅} × {𝑋})
∪ ({1𝑜} × {𝑌})) = (dom ({∅} × {𝑋}) ∪ dom
({1𝑜} × {𝑌})) |
11 | 9, 10 | eqtri 2632 |
. . . . . . 7
⊢ dom ◡({𝑋} +𝑐 {𝑌}) = (dom ({∅} × {𝑋}) ∪ dom
({1𝑜} × {𝑌})) |
12 | 7, 11 | syl6eleq 2698 |
. . . . . 6
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → ∅
∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌}))) |
13 | | elun 3715 |
. . . . . . 7
⊢ (∅
∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) ↔
(∅ ∈ dom ({∅} × {𝑋}) ∨ ∅ ∈ dom
({1𝑜} × {𝑌}))) |
14 | 2 | eldm 5243 |
. . . . . . . . 9
⊢ (∅
∈ dom ({∅} × {𝑋}) ↔ ∃𝑘∅({∅} × {𝑋})𝑘) |
15 | | brxp 5071 |
. . . . . . . . . . 11
⊢
(∅({∅} × {𝑋})𝑘 ↔ (∅ ∈ {∅} ∧ 𝑘 ∈ {𝑋})) |
16 | | elsni 4142 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑋} → 𝑘 = 𝑋) |
17 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑘 ∈ V |
18 | 16, 17 | syl6eqelr 2697 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑋} → 𝑋 ∈ V) |
19 | 18 | adantl 481 |
. . . . . . . . . . 11
⊢ ((∅
∈ {∅} ∧ 𝑘
∈ {𝑋}) → 𝑋 ∈ V) |
20 | 15, 19 | sylbi 206 |
. . . . . . . . . 10
⊢
(∅({∅} × {𝑋})𝑘 → 𝑋 ∈ V) |
21 | 20 | exlimiv 1845 |
. . . . . . . . 9
⊢
(∃𝑘∅({∅} × {𝑋})𝑘 → 𝑋 ∈ V) |
22 | 14, 21 | sylbi 206 |
. . . . . . . 8
⊢ (∅
∈ dom ({∅} × {𝑋}) → 𝑋 ∈ V) |
23 | | dmxpss 5484 |
. . . . . . . . . 10
⊢ dom
({1𝑜} × {𝑌}) ⊆
{1𝑜} |
24 | 23 | sseli 3564 |
. . . . . . . . 9
⊢ (∅
∈ dom ({1𝑜} × {𝑌}) → ∅ ∈
{1𝑜}) |
25 | | elsni 4142 |
. . . . . . . . 9
⊢ (∅
∈ {1𝑜} → ∅ =
1𝑜) |
26 | | 1n0 7462 |
. . . . . . . . . . . 12
⊢
1𝑜 ≠ ∅ |
27 | 26 | neii 2784 |
. . . . . . . . . . 11
⊢ ¬
1𝑜 = ∅ |
28 | 27 | pm2.21i 115 |
. . . . . . . . . 10
⊢
(1𝑜 = ∅ → 𝑋 ∈ V) |
29 | 28 | eqcoms 2618 |
. . . . . . . . 9
⊢ (∅
= 1𝑜 → 𝑋 ∈ V) |
30 | 24, 25, 29 | 3syl 18 |
. . . . . . . 8
⊢ (∅
∈ dom ({1𝑜} × {𝑌}) → 𝑋 ∈ V) |
31 | 22, 30 | jaoi 393 |
. . . . . . 7
⊢ ((∅
∈ dom ({∅} × {𝑋}) ∨ ∅ ∈ dom
({1𝑜} × {𝑌})) → 𝑋 ∈ V) |
32 | 13, 31 | sylbi 206 |
. . . . . 6
⊢ (∅
∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) → 𝑋 ∈ V) |
33 | 12, 32 | syl 17 |
. . . . 5
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → 𝑋 ∈ V) |
34 | | 1on 7454 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
35 | 34 | elexi 3186 |
. . . . . . . . . 10
⊢
1𝑜 ∈ V |
36 | 35 | prid2 4242 |
. . . . . . . . 9
⊢
1𝑜 ∈ {∅,
1𝑜} |
37 | 36, 4 | eleqtrri 2687 |
. . . . . . . 8
⊢
1𝑜 ∈ 2𝑜 |
38 | 37, 6 | syl5eleqr 2695 |
. . . . . . 7
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 →
1𝑜 ∈ dom ◡({𝑋} +𝑐 {𝑌})) |
39 | 38, 11 | syl6eleq 2698 |
. . . . . 6
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 →
1𝑜 ∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌}))) |
40 | | elun 3715 |
. . . . . . 7
⊢
(1𝑜 ∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) ↔
(1𝑜 ∈ dom ({∅} × {𝑋}) ∨ 1𝑜 ∈ dom
({1𝑜} × {𝑌}))) |
41 | | dmxpss 5484 |
. . . . . . . . . 10
⊢ dom
({∅} × {𝑋})
⊆ {∅} |
42 | 41 | sseli 3564 |
. . . . . . . . 9
⊢
(1𝑜 ∈ dom ({∅} × {𝑋}) → 1𝑜 ∈
{∅}) |
43 | | elsni 4142 |
. . . . . . . . 9
⊢
(1𝑜 ∈ {∅} → 1𝑜 =
∅) |
44 | 27 | pm2.21i 115 |
. . . . . . . . 9
⊢
(1𝑜 = ∅ → 𝑌 ∈ V) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . 8
⊢
(1𝑜 ∈ dom ({∅} × {𝑋}) → 𝑌 ∈ V) |
46 | 35 | eldm 5243 |
. . . . . . . . 9
⊢
(1𝑜 ∈ dom ({1𝑜} ×
{𝑌}) ↔ ∃𝑘1𝑜({1𝑜}
× {𝑌})𝑘) |
47 | | brxp 5071 |
. . . . . . . . . . 11
⊢
(1𝑜({1𝑜} × {𝑌})𝑘 ↔ (1𝑜 ∈
{1𝑜} ∧ 𝑘 ∈ {𝑌})) |
48 | | elsni 4142 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑌} → 𝑘 = 𝑌) |
49 | 48, 17 | syl6eqelr 2697 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑌} → 𝑌 ∈ V) |
50 | 49 | adantl 481 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ {1𝑜} ∧ 𝑘 ∈ {𝑌}) → 𝑌 ∈ V) |
51 | 47, 50 | sylbi 206 |
. . . . . . . . . 10
⊢
(1𝑜({1𝑜} × {𝑌})𝑘 → 𝑌 ∈ V) |
52 | 51 | exlimiv 1845 |
. . . . . . . . 9
⊢
(∃𝑘1𝑜({1𝑜}
× {𝑌})𝑘 → 𝑌 ∈ V) |
53 | 46, 52 | sylbi 206 |
. . . . . . . 8
⊢
(1𝑜 ∈ dom ({1𝑜} ×
{𝑌}) → 𝑌 ∈ V) |
54 | 45, 53 | jaoi 393 |
. . . . . . 7
⊢
((1𝑜 ∈ dom ({∅} × {𝑋}) ∨ 1𝑜 ∈ dom
({1𝑜} × {𝑌})) → 𝑌 ∈ V) |
55 | 40, 54 | sylbi 206 |
. . . . . 6
⊢
(1𝑜 ∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) → 𝑌 ∈ V) |
56 | 39, 55 | syl 17 |
. . . . 5
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → 𝑌 ∈ V) |
57 | 33, 56 | jca 553 |
. . . 4
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
58 | 57 | 3ad2ant1 1075 |
. . 3
⊢ ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
59 | | elex 3185 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V) |
60 | | elex 3185 |
. . . 4
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ V) |
61 | 59, 60 | anim12i 588 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
62 | | 3anass 1035 |
. . . 4
⊢ ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵))) |
63 | | xpscfn 16042 |
. . . . . 6
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ◡({𝑋} +𝑐 {𝑌}) Fn
2𝑜) |
64 | 63 | biantrurd 528 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵)))) |
65 | | xpsc0 16043 |
. . . . . . 7
⊢ (𝑋 ∈ V → (◡({𝑋} +𝑐 {𝑌})‘∅) = 𝑋) |
66 | 65 | eleq1d 2672 |
. . . . . 6
⊢ (𝑋 ∈ V → ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ↔ 𝑋 ∈ 𝐴)) |
67 | | xpsc1 16044 |
. . . . . . 7
⊢ (𝑌 ∈ V → (◡({𝑋} +𝑐 {𝑌})‘1𝑜) = 𝑌) |
68 | 67 | eleq1d 2672 |
. . . . . 6
⊢ (𝑌 ∈ V → ((◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵 ↔ 𝑌 ∈ 𝐵)) |
69 | 66, 68 | bi2anan9 913 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
70 | 64, 69 | bitr3d 269 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵)) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
71 | 62, 70 | syl5bb 271 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
72 | 58, 61, 71 | pm5.21nii 367 |
. 2
⊢ ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) |
73 | 1, 72 | bitri 263 |
1
⊢ (◡({𝑋} +𝑐 {𝑌}) ∈ X𝑘 ∈ 2𝑜
if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) |