Step | Hyp | Ref
| Expression |
1 | | xpomen 12124 |
. . . . 5
⊢ (ω
× ω) ≈ ω |
2 | 1 | ensymi 6727 |
. . . 4
⊢ ω
≈ (ω × ω) |
3 | | bren 6692 |
. . . 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 2157 |
. . . . . . . 8
⊢ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} = {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} |
8 | | eqid 2157 |
. . . . . . . 8
⊢ (◡inl ∘ 𝐹) = (◡inl ∘ 𝐹) |
9 | 6, 7, 8 | ctssdccl 7055 |
. . . . . . 7
⊢ (𝜑 → ({𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω ∧ (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)})) |
10 | 9 | simp1d 994 |
. . . . . 6
⊢ (𝜑 → {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω) |
11 | 10 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ⊆ ω) |
12 | 9 | simp3d 996 |
. . . . . 6
⊢ (𝜑 → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}) |
13 | 12 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) →
∀𝑛 ∈ ω
DECID 𝑛
∈ {𝑤 ∈ ω
∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}) |
14 | 9 | simp2d 995 |
. . . . . 6
⊢ (𝜑 → (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴) |
15 | 14 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → (◡inl ∘ 𝐹):{𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)}–onto→𝐴) |
16 | | ctiunct.b |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺:ω–onto→(𝐵 ⊔ 1o)) |
17 | | eqid 2157 |
. . . . . . . 8
⊢ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} = {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} |
18 | | eqid 2157 |
. . . . . . . 8
⊢ (◡inl ∘ 𝐺) = (◡inl ∘ 𝐺) |
19 | 16, 17, 18 | ctssdccl 7055 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω ∧ (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})) |
20 | 19 | simp1d 994 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω) |
21 | 20 | adantlr 469 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} ⊆ ω) |
22 | 19 | simp3d 996 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}) |
23 | 22 | adantlr 469 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}) |
24 | 19 | simp2d 995 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵) |
25 | 24 | adantlr 469 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) ∧ 𝑥 ∈ 𝐴) → (◡inl ∘ 𝐺):{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}–onto→𝐵) |
26 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → 𝑗:ω–1-1-onto→(ω × ω)) |
27 | | eqid 2157 |
. . . . 5
⊢ {𝑧 ∈ ω ∣
((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} |
28 | 11, 13, 15, 21, 23, 25, 26, 27 | ctiunctlemuom 12165 |
. . . 4
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → {𝑧 ∈ ω ∣
((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω) |
29 | | eqid 2157 |
. . . . . 6
⊢ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) = (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) |
30 | | nfv 1508 |
. . . . . . . . 9
⊢
Ⅎ𝑥(1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} |
31 | | nfcsb1v 3064 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} |
32 | 31 | nfel2 2312 |
. . . . . . . . 9
⊢
Ⅎ𝑥(2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)} |
33 | 30, 32 | nfan 1545 |
. . . . . . . 8
⊢
Ⅎ𝑥((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)}) |
34 | | nfcv 2299 |
. . . . . . . 8
⊢
Ⅎ𝑥ω |
35 | 33, 34 | nfrabxy 2637 |
. . . . . . 7
⊢
Ⅎ𝑥{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} |
36 | | nfcsb1v 3064 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺) |
37 | | nfcv 2299 |
. . . . . . . 8
⊢
Ⅎ𝑥(2nd ‘(𝑗‘𝑛)) |
38 | 36, 37 | nffv 5478 |
. . . . . . 7
⊢
Ⅎ𝑥(⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛))) |
39 | 35, 38 | nfmpt 4056 |
. . . . . 6
⊢
Ⅎ𝑥(𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) |
40 | 11, 13, 15, 21, 23, 25, 26, 27, 29, 39, 35 | ctiunctlemfo 12168 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))):{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵) |
41 | | omex 4552 |
. . . . . . . 8
⊢ ω
∈ V |
42 | 41 | rabex 4108 |
. . . . . . 7
⊢ {𝑧 ∈ ω ∣
((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ∈ V |
43 | 42 | mptex 5693 |
. . . . . 6
⊢ (𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ↦ (⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑛))) / 𝑥⦌(◡inl ∘ 𝐺)‘(2nd ‘(𝑗‘𝑛)))) ∈ V |
44 | | foeq1 5388 |
. . . . . 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 2807 |
. . . . 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 12166 |
. . . 4
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) →
∀𝑛 ∈ ω
DECID 𝑛
∈ {𝑧 ∈ ω
∣ ((1st ‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}) |
48 | | sseq1 3151 |
. . . . . 6
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑢 ⊆ ω ↔ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} ⊆ ω)) |
49 | | foeq2 5389 |
. . . . . . 7
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)) |
50 | 49 | exbidv 1805 |
. . . . . 6
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑘 𝑘:{𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})}–onto→∪ 𝑥 ∈ 𝐴 𝐵)) |
51 | | eleq2 2221 |
. . . . . . . 8
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (𝑛 ∈ 𝑢 ↔ 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})) |
52 | 51 | dcbid 824 |
. . . . . . 7
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (DECID 𝑛 ∈ 𝑢 ↔ DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})) |
53 | 52 | ralbidv 2457 |
. . . . . 6
⊢ (𝑢 = {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})} → (∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢 ↔ ∀𝑛 ∈ ω DECID 𝑛 ∈ {𝑧 ∈ ω ∣ ((1st
‘(𝑗‘𝑧)) ∈ {𝑤 ∈ ω ∣ (𝐹‘𝑤) ∈ (inl “ 𝐴)} ∧ (2nd ‘(𝑗‘𝑧)) ∈ ⦋((◡inl ∘ 𝐹)‘(1st ‘(𝑗‘𝑧))) / 𝑥⦌{𝑤 ∈ ω ∣ (𝐺‘𝑤) ∈ (inl “ 𝐵)})})) |
54 | 48, 50, 53 | 3anbi123d 1294 |
. . . . 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 2807 |
. . . 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 1220 |
. . 3
⊢ ((𝜑 ∧ 𝑗:ω–1-1-onto→(ω × ω)) → ∃𝑢(𝑢 ⊆ ω ∧ ∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢)) |
57 | | ctssdc 7057 |
. . . 4
⊢
(∃𝑢(𝑢 ⊆ ω ∧
∃𝑘 𝑘:𝑢–onto→∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑛 ∈ ω DECID 𝑛 ∈ 𝑢) ↔ ∃𝑘 𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) |
58 | | foeq1 5388 |
. . . . 5
⊢ (𝑘 = ℎ → (𝑘:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o) ↔ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o))) |
59 | 58 | cbvexv 1898 |
. . . 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 1878 |
1
⊢ (𝜑 → ∃ℎ ℎ:ω–onto→(∪ 𝑥 ∈ 𝐴 𝐵 ⊔ 1o)) |