Proof of Theorem xpsfrnel2
Step | Hyp | Ref
| Expression |
1 | | xpsfrnel 16223 |
. 2
⊢ (◡({𝑋} +𝑐 {𝑌}) ∈ X𝑘 ∈ 2𝑜
if(𝑘 = ∅, 𝐴, 𝐵) ↔ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵)) |
2 | | 0ex 4790 |
. . . . . . . . . 10
⊢ ∅
∈ V |
3 | 2 | prid1 4297 |
. . . . . . . . 9
⊢ ∅
∈ {∅, 1𝑜} |
4 | | df2o3 7573 |
. . . . . . . . 9
⊢
2𝑜 = {∅,
1𝑜} |
5 | 3, 4 | eleqtrri 2700 |
. . . . . . . 8
⊢ ∅
∈ 2𝑜 |
6 | | fndm 5990 |
. . . . . . . 8
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → dom ◡({𝑋} +𝑐 {𝑌}) = 2𝑜) |
7 | 5, 6 | syl5eleqr 2708 |
. . . . . . 7
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → ∅
∈ dom ◡({𝑋} +𝑐 {𝑌})) |
8 | | xpsc 16217 |
. . . . . . . . 9
⊢ ◡({𝑋} +𝑐 {𝑌}) = (({∅} × {𝑋}) ∪ ({1𝑜} ×
{𝑌})) |
9 | 8 | dmeqi 5325 |
. . . . . . . 8
⊢ dom ◡({𝑋} +𝑐 {𝑌}) = dom (({∅} × {𝑋}) ∪
({1𝑜} × {𝑌})) |
10 | | dmun 5331 |
. . . . . . . 8
⊢ dom
(({∅} × {𝑋})
∪ ({1𝑜} × {𝑌})) = (dom ({∅} × {𝑋}) ∪ dom
({1𝑜} × {𝑌})) |
11 | 9, 10 | eqtri 2644 |
. . . . . . 7
⊢ dom ◡({𝑋} +𝑐 {𝑌}) = (dom ({∅} × {𝑋}) ∪ dom
({1𝑜} × {𝑌})) |
12 | 7, 11 | syl6eleq 2711 |
. . . . . 6
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → ∅
∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌}))) |
13 | | elun 3753 |
. . . . . . 7
⊢ (∅
∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) ↔
(∅ ∈ dom ({∅} × {𝑋}) ∨ ∅ ∈ dom
({1𝑜} × {𝑌}))) |
14 | 2 | eldm 5321 |
. . . . . . . . 9
⊢ (∅
∈ dom ({∅} × {𝑋}) ↔ ∃𝑘∅({∅} × {𝑋})𝑘) |
15 | | brxp 5147 |
. . . . . . . . . . 11
⊢
(∅({∅} × {𝑋})𝑘 ↔ (∅ ∈ {∅} ∧ 𝑘 ∈ {𝑋})) |
16 | | elsni 4194 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑋} → 𝑘 = 𝑋) |
17 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑘 ∈ V |
18 | 16, 17 | syl6eqelr 2710 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑋} → 𝑋 ∈ V) |
19 | 18 | adantl 482 |
. . . . . . . . . . 11
⊢ ((∅
∈ {∅} ∧ 𝑘
∈ {𝑋}) → 𝑋 ∈ V) |
20 | 15, 19 | sylbi 207 |
. . . . . . . . . 10
⊢
(∅({∅} × {𝑋})𝑘 → 𝑋 ∈ V) |
21 | 20 | exlimiv 1858 |
. . . . . . . . 9
⊢
(∃𝑘∅({∅} × {𝑋})𝑘 → 𝑋 ∈ V) |
22 | 14, 21 | sylbi 207 |
. . . . . . . 8
⊢ (∅
∈ dom ({∅} × {𝑋}) → 𝑋 ∈ V) |
23 | | dmxpss 5565 |
. . . . . . . . . 10
⊢ dom
({1𝑜} × {𝑌}) ⊆
{1𝑜} |
24 | 23 | sseli 3599 |
. . . . . . . . 9
⊢ (∅
∈ dom ({1𝑜} × {𝑌}) → ∅ ∈
{1𝑜}) |
25 | | elsni 4194 |
. . . . . . . . 9
⊢ (∅
∈ {1𝑜} → ∅ =
1𝑜) |
26 | | 1n0 7575 |
. . . . . . . . . . . 12
⊢
1𝑜 ≠ ∅ |
27 | 26 | neii 2796 |
. . . . . . . . . . 11
⊢ ¬
1𝑜 = ∅ |
28 | 27 | pm2.21i 116 |
. . . . . . . . . 10
⊢
(1𝑜 = ∅ → 𝑋 ∈ V) |
29 | 28 | eqcoms 2630 |
. . . . . . . . 9
⊢ (∅
= 1𝑜 → 𝑋 ∈ V) |
30 | 24, 25, 29 | 3syl 18 |
. . . . . . . 8
⊢ (∅
∈ dom ({1𝑜} × {𝑌}) → 𝑋 ∈ V) |
31 | 22, 30 | jaoi 394 |
. . . . . . 7
⊢ ((∅
∈ dom ({∅} × {𝑋}) ∨ ∅ ∈ dom
({1𝑜} × {𝑌})) → 𝑋 ∈ V) |
32 | 13, 31 | sylbi 207 |
. . . . . 6
⊢ (∅
∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) → 𝑋 ∈ V) |
33 | 12, 32 | syl 17 |
. . . . 5
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → 𝑋 ∈ V) |
34 | | 1on 7567 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
35 | 34 | elexi 3213 |
. . . . . . . . . 10
⊢
1𝑜 ∈ V |
36 | 35 | prid2 4298 |
. . . . . . . . 9
⊢
1𝑜 ∈ {∅,
1𝑜} |
37 | 36, 4 | eleqtrri 2700 |
. . . . . . . 8
⊢
1𝑜 ∈ 2𝑜 |
38 | 37, 6 | syl5eleqr 2708 |
. . . . . . 7
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 →
1𝑜 ∈ dom ◡({𝑋} +𝑐 {𝑌})) |
39 | 38, 11 | syl6eleq 2711 |
. . . . . 6
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 →
1𝑜 ∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌}))) |
40 | | elun 3753 |
. . . . . . 7
⊢
(1𝑜 ∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) ↔
(1𝑜 ∈ dom ({∅} × {𝑋}) ∨ 1𝑜 ∈ dom
({1𝑜} × {𝑌}))) |
41 | | dmxpss 5565 |
. . . . . . . . . 10
⊢ dom
({∅} × {𝑋})
⊆ {∅} |
42 | 41 | sseli 3599 |
. . . . . . . . 9
⊢
(1𝑜 ∈ dom ({∅} × {𝑋}) → 1𝑜 ∈
{∅}) |
43 | | elsni 4194 |
. . . . . . . . 9
⊢
(1𝑜 ∈ {∅} → 1𝑜 =
∅) |
44 | 27 | pm2.21i 116 |
. . . . . . . . 9
⊢
(1𝑜 = ∅ → 𝑌 ∈ V) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . 8
⊢
(1𝑜 ∈ dom ({∅} × {𝑋}) → 𝑌 ∈ V) |
46 | 35 | eldm 5321 |
. . . . . . . . 9
⊢
(1𝑜 ∈ dom ({1𝑜} ×
{𝑌}) ↔ ∃𝑘1𝑜({1𝑜}
× {𝑌})𝑘) |
47 | | brxp 5147 |
. . . . . . . . . . 11
⊢
(1𝑜({1𝑜} × {𝑌})𝑘 ↔ (1𝑜 ∈
{1𝑜} ∧ 𝑘 ∈ {𝑌})) |
48 | | elsni 4194 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ {𝑌} → 𝑘 = 𝑌) |
49 | 48, 17 | syl6eqelr 2710 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ {𝑌} → 𝑌 ∈ V) |
50 | 49 | adantl 482 |
. . . . . . . . . . 11
⊢
((1𝑜 ∈ {1𝑜} ∧ 𝑘 ∈ {𝑌}) → 𝑌 ∈ V) |
51 | 47, 50 | sylbi 207 |
. . . . . . . . . 10
⊢
(1𝑜({1𝑜} × {𝑌})𝑘 → 𝑌 ∈ V) |
52 | 51 | exlimiv 1858 |
. . . . . . . . 9
⊢
(∃𝑘1𝑜({1𝑜}
× {𝑌})𝑘 → 𝑌 ∈ V) |
53 | 46, 52 | sylbi 207 |
. . . . . . . 8
⊢
(1𝑜 ∈ dom ({1𝑜} ×
{𝑌}) → 𝑌 ∈ V) |
54 | 45, 53 | jaoi 394 |
. . . . . . 7
⊢
((1𝑜 ∈ dom ({∅} × {𝑋}) ∨ 1𝑜 ∈ dom
({1𝑜} × {𝑌})) → 𝑌 ∈ V) |
55 | 40, 54 | sylbi 207 |
. . . . . 6
⊢
(1𝑜 ∈ (dom ({∅} × {𝑋}) ∪ dom ({1𝑜}
× {𝑌})) → 𝑌 ∈ V) |
56 | 39, 55 | syl 17 |
. . . . 5
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → 𝑌 ∈ V) |
57 | 33, 56 | jca 554 |
. . . 4
⊢ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
58 | 57 | 3ad2ant1 1082 |
. . 3
⊢ ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
59 | | elex 3212 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V) |
60 | | elex 3212 |
. . . 4
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ V) |
61 | 59, 60 | anim12i 590 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
62 | | 3anass 1042 |
. . . 4
⊢ ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵))) |
63 | | xpscfn 16219 |
. . . . . 6
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ◡({𝑋} +𝑐 {𝑌}) Fn
2𝑜) |
64 | 63 | biantrurd 529 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵)))) |
65 | | xpsc0 16220 |
. . . . . . 7
⊢ (𝑋 ∈ V → (◡({𝑋} +𝑐 {𝑌})‘∅) = 𝑋) |
66 | 65 | eleq1d 2686 |
. . . . . 6
⊢ (𝑋 ∈ V → ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ↔ 𝑋 ∈ 𝐴)) |
67 | | xpsc1 16221 |
. . . . . . 7
⊢ (𝑌 ∈ V → (◡({𝑋} +𝑐 {𝑌})‘1𝑜) = 𝑌) |
68 | 67 | eleq1d 2686 |
. . . . . 6
⊢ (𝑌 ∈ V → ((◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵 ↔ 𝑌 ∈ 𝐵)) |
69 | 66, 68 | bi2anan9 917 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
70 | 64, 69 | bitr3d 270 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ ((◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵)) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
71 | 62, 70 | syl5bb 272 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
72 | 58, 61, 71 | pm5.21nii 368 |
. 2
⊢ ((◡({𝑋} +𝑐 {𝑌}) Fn 2𝑜 ∧ (◡({𝑋} +𝑐 {𝑌})‘∅) ∈ 𝐴 ∧ (◡({𝑋} +𝑐 {𝑌})‘1𝑜) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) |
73 | 1, 72 | bitri 264 |
1
⊢ (◡({𝑋} +𝑐 {𝑌}) ∈ X𝑘 ∈ 2𝑜
if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) |