Step | Hyp | Ref
| Expression |
1 | | eliun 4460 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) ↔ ∃𝑘 ∈ ω 𝑦 ∈ (𝐴 ↑𝑚 𝑘)) |
2 | | elmapi 7765 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴 ↑𝑚 𝑘) → 𝑦:𝑘⟶𝐴) |
3 | 2 | ad2antll 761 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 𝑦:𝑘⟶𝐴) |
4 | | fdm 5964 |
. . . . . . . . 9
⊢ (𝑦:𝑘⟶𝐴 → dom 𝑦 = 𝑘) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → dom 𝑦 = 𝑘) |
6 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 𝑘 ∈ ω) |
7 | 5, 6 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → dom 𝑦 ∈
ω) |
8 | 5 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → (𝐺‘dom 𝑦) = (𝐺‘𝑘)) |
9 | 8 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → ((𝐺‘dom 𝑦)‘𝑦) = ((𝐺‘𝑘)‘𝑦)) |
10 | | fseqenlem.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
11 | | fseqenlem.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
12 | | fseqenlem.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) |
13 | | fseqenlem.g |
. . . . . . . . . . . 12
⊢ 𝐺 =
seq𝜔((𝑛
∈ V, 𝑓 ∈ V
↦ (𝑥 ∈ (𝐴 ↑𝑚 suc
𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) |
14 | 10, 11, 12, 13 | fseqenlem1 8730 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)–1-1→𝐴) |
15 | 14 | adantrr 749 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)–1-1→𝐴) |
16 | | f1f 6014 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)–1-1→𝐴 → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)⟶𝐴) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)⟶𝐴) |
18 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 𝑦 ∈ (𝐴 ↑𝑚 𝑘)) |
19 | 17, 18 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → ((𝐺‘𝑘)‘𝑦) ∈ 𝐴) |
20 | 9, 19 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → ((𝐺‘dom 𝑦)‘𝑦) ∈ 𝐴) |
21 | | opelxpi 5072 |
. . . . . . 7
⊢ ((dom
𝑦 ∈ ω ∧
((𝐺‘dom 𝑦)‘𝑦) ∈ 𝐴) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
22 | 7, 20, 21 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
23 | 22 | rexlimdvaa 3014 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ω 𝑦 ∈ (𝐴 ↑𝑚 𝑘) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴))) |
24 | 1, 23 | syl5bi 231 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴))) |
25 | 24 | imp 444 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
26 | | fseqenlem.k |
. . 3
⊢ 𝐾 = (𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘) ↦ 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉) |
27 | 25, 26 | fmptd 6292 |
. 2
⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)⟶(ω ×
𝐴)) |
28 | | ffun 5961 |
. . . . . . . . . . . . . . 15
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)⟶(ω × 𝐴) → Fun 𝐾) |
29 | | funbrfv2b 6150 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝐾 → (𝑧𝐾𝑤 ↔ (𝑧 ∈ dom 𝐾 ∧ (𝐾‘𝑧) = 𝑤))) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑧𝐾𝑤 ↔ (𝑧 ∈ dom 𝐾 ∧ (𝐾‘𝑧) = 𝑤))) |
31 | 30 | simplbda 652 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐾‘𝑧) = 𝑤) |
32 | 30 | simprbda 651 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ dom 𝐾) |
33 | | fdm 5964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)⟶(ω × 𝐴) → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
36 | 32, 35 | eleqtrd 2690 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
37 | | dmeq 5246 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → dom 𝑦 = dom 𝑧) |
38 | 37 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝐺‘dom 𝑦) = (𝐺‘dom 𝑧)) |
39 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
40 | 38, 39 | fveq12d 6109 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → ((𝐺‘dom 𝑦)‘𝑦) = ((𝐺‘dom 𝑧)‘𝑧)) |
41 | 37, 40 | opeq12d 4348 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
42 | | opex 4859 |
. . . . . . . . . . . . . . 15
⊢ 〈dom
𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉 ∈ V |
43 | 41, 26, 42 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) → (𝐾‘𝑧) = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
44 | 36, 43 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐾‘𝑧) = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
45 | 31, 44 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑤 = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
46 | 45 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (1st ‘𝑤) = (1st
‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉)) |
47 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
48 | 47 | dmex 6991 |
. . . . . . . . . . . 12
⊢ dom 𝑧 ∈ V |
49 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ ((𝐺‘dom 𝑧)‘𝑧) ∈ V |
50 | 48, 49 | op1st 7067 |
. . . . . . . . . . 11
⊢
(1st ‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) = dom 𝑧 |
51 | 46, 50 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (1st ‘𝑤) = dom 𝑧) |
52 | 51 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘(1st ‘𝑤)) = (𝐺‘dom 𝑧)) |
53 | 52 | cnveqd 5220 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → ◡(𝐺‘(1st ‘𝑤)) = ◡(𝐺‘dom 𝑧)) |
54 | 45 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (2nd ‘𝑤) = (2nd
‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉)) |
55 | 48, 49 | op2nd 7068 |
. . . . . . . . 9
⊢
(2nd ‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) = ((𝐺‘dom 𝑧)‘𝑧) |
56 | 54, 55 | syl6eq 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (2nd ‘𝑤) = ((𝐺‘dom 𝑧)‘𝑧)) |
57 | 53, 56 | fveq12d 6109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)) = (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧))) |
58 | | eliun 4460 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) ↔ ∃𝑘 ∈ ω 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) |
59 | | elmapi 7765 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝐴 ↑𝑚 𝑘) → 𝑧:𝑘⟶𝐴) |
60 | 59 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑧:𝑘⟶𝐴) |
61 | | fdm 5964 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧:𝑘⟶𝐴 → dom 𝑧 = 𝑘) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → dom 𝑧 = 𝑘) |
63 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑘 ∈ ω) |
64 | 62, 63 | eqeltrd 2688 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → dom 𝑧 ∈ ω) |
65 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) |
66 | 62 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → (𝐴 ↑𝑚 dom 𝑧) = (𝐴 ↑𝑚 𝑘)) |
67 | 65, 66 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧)) |
68 | 64, 67 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
69 | 68 | rexlimiva 3010 |
. . . . . . . . . . . . 13
⊢
(∃𝑘 ∈
ω 𝑧 ∈ (𝐴 ↑𝑚
𝑘) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
70 | 58, 69 | sylbi 206 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
71 | 36, 70 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
72 | 71 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → dom 𝑧 ∈ ω) |
73 | 10, 11, 12, 13 | fseqenlem1 8730 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑧 ∈ ω) → (𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1→𝐴) |
74 | 72, 73 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1→𝐴) |
75 | | f1f1orn 6061 |
. . . . . . . . 9
⊢ ((𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1→𝐴 → (𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1-onto→ran
(𝐺‘dom 𝑧)) |
76 | 74, 75 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1-onto→ran
(𝐺‘dom 𝑧)) |
77 | 71 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧)) |
78 | | f1ocnvfv1 6432 |
. . . . . . . 8
⊢ (((𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1-onto→ran
(𝐺‘dom 𝑧) ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧)) → (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧)) = 𝑧) |
79 | 76, 77, 78 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧)) = 𝑧) |
80 | 57, 79 | eqtr2d 2645 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤))) |
81 | 80 | ex 449 |
. . . . 5
⊢ (𝜑 → (𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)))) |
82 | 81 | alrimiv 1842 |
. . . 4
⊢ (𝜑 → ∀𝑧(𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)))) |
83 | | mo2icl 3352 |
. . . 4
⊢
(∀𝑧(𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤))) →
∃*𝑧 𝑧𝐾𝑤) |
84 | 82, 83 | syl 17 |
. . 3
⊢ (𝜑 → ∃*𝑧 𝑧𝐾𝑤) |
85 | 84 | alrimiv 1842 |
. 2
⊢ (𝜑 → ∀𝑤∃*𝑧 𝑧𝐾𝑤) |
86 | | dff12 6013 |
. 2
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)–1-1→(ω × 𝐴) ↔ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)⟶(ω ×
𝐴) ∧ ∀𝑤∃*𝑧 𝑧𝐾𝑤)) |
87 | 27, 85, 86 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)–1-1→(ω × 𝐴)) |