Step | Hyp | Ref
| Expression |
1 | | xpomen 12350 |
. . . . 5
⊢ (ω
× ω) ≈ ω |
2 | 1 | ensymi 6760 |
. . . 4
⊢ ω
≈ (ω × ω) |
3 | | bren 6725 |
. . . 4
⊢ (ω
≈ (ω × ω) ↔ ∃𝑗 𝑗:ω–1-1-onto→(ω × ω)) |
4 | 2, 3 | mpbi 144 |
. . 3
⊢
∃𝑗 𝑗:ω–1-1-onto→(ω × ω) |
5 | 4 | a1i 9 |
. 2
⊢ (𝜑 → ∃𝑗 𝑗:ω–1-1-onto→(ω × ω)) |
6 | | ctiunct.a |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ω–onto→(𝐴 ⊔ 1o)) |
7 | | eqid 2170 |
. . . . . . . 8
⊢ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} = {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} |
8 | | eqid 2170 |
. . . . . . . 8
⊢ (◡inl ∘ 𝐹) = (◡inl ∘ 𝐹) |
9 | 6, 7, 8 | ctssdccl 7088 |
. . . . . . 7
⊢ (𝜑 → ({𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω ∧ (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)})) |
10 | 9 | simp1d 1004 |
. . . . . 6
⊢ (𝜑 → {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω) |
11 | 10 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω) |
12 | 9 | simp3d 1006 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}) |
13 | 12 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) →
∀𝑛 ∈ ω
DECID 𝑛
∈ {𝑤 ∈ ω
∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}) |
14 | 9 | simp2d 1005 |
. . . . . 6
⊢ (𝜑 → (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴) |
15 | 14 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴) |
16 | | ctiunct.b |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o)) |
17 | | eqid 2170 |
. . . . . . . 8
⊢ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} = {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} |
18 | | eqid 2170 |
. . . . . . . 8
⊢ (◡inl ∘ 𝐺) = (◡inl ∘ 𝐺) |
19 | 16, 17, 18 | ctssdccl 7088 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω ∧ (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})) |
20 | 19 | simp1d 1004 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω) |
21 | 20 | adantlr 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω) |
22 | 19 | simp3d 1006 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}) |
23 | 22 | adantlr 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}) |
24 | 19 | simp2d 1005 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵) |
25 | 24 | adantlr 474 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵) |
26 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → 𝑗:ω–1-1-onto→(ω × ω)) |
27 | | eqid 2170 |
. . . . 5
⊢ {𝑧 ∈ ω ∣
((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} |
28 | 11, 13, 15, 21, 23, 25, 26, 27 | ctiunctlemuom 12391 |
. . . 4
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → {𝑧 ∈ ω ∣
((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω) |
29 | | eqid 2170 |
. . . . . 6
⊢ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) = (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) |
30 | | nfv 1521 |
. . . . . . . . 9
⊢
Ⅎ𝑥(1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} |
31 | | nfcsb1v 3082 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} |
32 | 31 | nfel2 2325 |
. . . . . . . . 9
⊢
Ⅎ𝑥(2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} |
33 | 30, 32 | nfan 1558 |
. . . . . . . 8
⊢
Ⅎ𝑥((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}) |
34 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑥ω |
35 | 33, 34 | nfrabxy 2650 |
. . . . . . 7
⊢
Ⅎ𝑥{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} |
36 | | nfcsb1v 3082 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺) |
37 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑥(2nd ‘(𝑗‘𝑛)) |
38 | 36, 37 | nffv 5506 |
. . . . . . 7
⊢
Ⅎ𝑥(⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛))) |
39 | 35, 38 | nfmpt 4081 |
. . . . . 6
⊢
Ⅎ𝑥(𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) |
40 | 11, 13, 15, 21, 23, 25, 26, 27, 29, 39, 35 | ctiunctlemfo 12394 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))):{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵) |
41 | | omex 4577 |
. . . . . . . 8
⊢ ω
∈ V |
42 | 41 | rabex 4133 |
. . . . . . 7
⊢ {𝑧 ∈ ω ∣
((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ∈ V |
43 | 42 | mptex 5722 |
. . . . . 6
⊢ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) ∈ V |
44 | | foeq1 5416 |
. . . . . 6
⊢ (𝑘 = (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) → (𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))):{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)) |
45 | 43, 44 | spcev 2825 |
. . . . 5
⊢ ((𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))):{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵) |
46 | 40, 45 | syl 14 |
. . . 4
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵) |
47 | 11, 13, 15, 21, 23, 25, 26, 27 | ctiunctlemudc 12392 |
. . . 4
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) →
∀𝑛 ∈ ω
DECID 𝑛
∈ {𝑧 ∈ ω
∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}) |
48 | | sseq1 3170 |
. . . . . 6
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑢 ⊆ ω ↔ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω)) |
49 | | foeq2 5417 |
. . . . . . 7
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)) |
50 | 49 | exbidv 1818 |
. . . . . 6
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)) |
51 | | eleq2 2234 |
. . . . . . . 8
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑛 ∈ 𝑢 ↔ 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})) |
52 | 51 | dcbid 833 |
. . . . . . 7
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (DECID 𝑛 ∈ 𝑢 ↔ DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})) |
53 | 52 | ralbidv 2470 |
. . . . . 6
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢 ↔ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})) |
54 | 48, 50, 53 | 3anbi123d 1307 |
. . . . 5
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → ((𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢) ↔ ({𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω ∧ ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}))) |
55 | 42, 54 | spcev 2825 |
. . . 4
⊢ (({𝑧 ∈ ω ∣
((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω ∧ ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}) → ∃𝑢(𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢)) |
56 | 28, 46, 47, 55 | syl3anc 1233 |
. . 3
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∃𝑢(𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢)) |
57 | | ctssdc 7090 |
. . . 4
⊢
(∃𝑢(𝑢 ⊆ ω ∧
∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢) ↔ ∃𝑘 𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) |
58 | | foeq1 5416 |
. . . . 5
⊢ (𝑘 = ℎ → (𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o) ↔ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))) |
59 | 58 | cbvexv 1911 |
. . . 4
⊢
(∃𝑘 𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o) ↔ ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) |
60 | 57, 59 | bitri 183 |
. . 3
⊢
(∃𝑢(𝑢 ⊆ ω ∧
∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢) ↔ ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) |
61 | 56, 60 | sylib 121 |
. 2
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) |
62 | 5, 61 | exlimddv 1891 |
1
⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) |