Step | Hyp | Ref
| Expression |
1 | | eliun 4524 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) ↔ ∃𝑘 ∈ ω 𝑦 ∈ (𝐴 ↑𝑚 𝑘)) |
2 | | elmapi 7879 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴 ↑𝑚 𝑘) → 𝑦:𝑘⟶𝐴) |
3 | 2 | ad2antll 765 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 𝑦:𝑘⟶𝐴) |
4 | | fdm 6051 |
. . . . . . . . 9
⊢ (𝑦:𝑘⟶𝐴 → dom 𝑦 = 𝑘) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → dom 𝑦 = 𝑘) |
6 | | simprl 794 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 𝑘 ∈ ω) |
7 | 5, 6 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → dom 𝑦 ∈
ω) |
8 | 5 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → (𝐺‘dom 𝑦) = (𝐺‘𝑘)) |
9 | 8 | fveq1d 6193 |
. . . . . . . 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 8847 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)–1-1→𝐴) |
15 | 14 | adantrr 753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)–1-1→𝐴) |
16 | | f1f 6101 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)–1-1→𝐴 → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)⟶𝐴) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → (𝐺‘𝑘):(𝐴 ↑𝑚 𝑘)⟶𝐴) |
18 | | simprr 796 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 𝑦 ∈ (𝐴 ↑𝑚 𝑘)) |
19 | 17, 18 | ffvelrnd 6360 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → ((𝐺‘𝑘)‘𝑦) ∈ 𝐴) |
20 | 9, 19 | eqeltrd 2701 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → ((𝐺‘dom 𝑦)‘𝑦) ∈ 𝐴) |
21 | | opelxpi 5148 |
. . . . . . 7
⊢ ((dom
𝑦 ∈ ω ∧
((𝐺‘dom 𝑦)‘𝑦) ∈ 𝐴) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
22 | 7, 20, 21 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑𝑚 𝑘))) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
23 | 22 | rexlimdvaa 3032 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ω 𝑦 ∈ (𝐴 ↑𝑚 𝑘) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴))) |
24 | 1, 23 | syl5bi 232 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴))) |
25 | 24 | imp 445 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
26 | | fseqenlem.k |
. . 3
⊢ 𝐾 = (𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘) ↦ 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉) |
27 | 25, 26 | fmptd 6385 |
. 2
⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)⟶(ω ×
𝐴)) |
28 | | ffun 6048 |
. . . . . . . . . . . . . . 15
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)⟶(ω × 𝐴) → Fun 𝐾) |
29 | | funbrfv2b 6240 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝐾 → (𝑧𝐾𝑤 ↔ (𝑧 ∈ dom 𝐾 ∧ (𝐾‘𝑧) = 𝑤))) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑧𝐾𝑤 ↔ (𝑧 ∈ dom 𝐾 ∧ (𝐾‘𝑧) = 𝑤))) |
31 | 30 | simplbda 654 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐾‘𝑧) = 𝑤) |
32 | 30 | simprbda 653 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ dom 𝐾) |
33 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)⟶(ω × 𝐴) → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
36 | 32, 35 | eleqtrd 2703 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ ∪
𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)) |
37 | | dmeq 5324 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → dom 𝑦 = dom 𝑧) |
38 | 37 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝐺‘dom 𝑦) = (𝐺‘dom 𝑧)) |
39 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
40 | 38, 39 | fveq12d 6197 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → ((𝐺‘dom 𝑦)‘𝑦) = ((𝐺‘dom 𝑧)‘𝑧)) |
41 | 37, 40 | opeq12d 4410 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
42 | | opex 4932 |
. . . . . . . . . . . . . . 15
⊢ 〈dom
𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉 ∈ V |
43 | 41, 26, 42 | fvmpt 6282 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) → (𝐾‘𝑧) = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
44 | 36, 43 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐾‘𝑧) = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
45 | 31, 44 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑤 = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
46 | 45 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (1st ‘𝑤) = (1st
‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉)) |
47 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
48 | 47 | dmex 7099 |
. . . . . . . . . . . 12
⊢ dom 𝑧 ∈ V |
49 | | fvex 6201 |
. . . . . . . . . . . 12
⊢ ((𝐺‘dom 𝑧)‘𝑧) ∈ V |
50 | 48, 49 | op1st 7176 |
. . . . . . . . . . 11
⊢
(1st ‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) = dom 𝑧 |
51 | 46, 50 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (1st ‘𝑤) = dom 𝑧) |
52 | 51 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘(1st ‘𝑤)) = (𝐺‘dom 𝑧)) |
53 | 52 | cnveqd 5298 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → ◡(𝐺‘(1st ‘𝑤)) = ◡(𝐺‘dom 𝑧)) |
54 | 45 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (2nd ‘𝑤) = (2nd
‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉)) |
55 | 48, 49 | op2nd 7177 |
. . . . . . . . 9
⊢
(2nd ‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) = ((𝐺‘dom 𝑧)‘𝑧) |
56 | 54, 55 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (2nd ‘𝑤) = ((𝐺‘dom 𝑧)‘𝑧)) |
57 | 53, 56 | fveq12d 6197 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)) = (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧))) |
58 | | eliun 4524 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) ↔ ∃𝑘 ∈ ω 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) |
59 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝐴 ↑𝑚 𝑘) → 𝑧:𝑘⟶𝐴) |
60 | 59 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑧:𝑘⟶𝐴) |
61 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧:𝑘⟶𝐴 → dom 𝑧 = 𝑘) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → dom 𝑧 = 𝑘) |
63 | | simpl 473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑘 ∈ ω) |
64 | 62, 63 | eqeltrd 2701 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → dom 𝑧 ∈ ω) |
65 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) |
66 | 62 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → (𝐴 ↑𝑚 dom 𝑧) = (𝐴 ↑𝑚 𝑘)) |
67 | 65, 66 | eleqtrrd 2704 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧)) |
68 | 64, 67 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 𝑘)) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
69 | 68 | rexlimiva 3028 |
. . . . . . . . . . . . 13
⊢
(∃𝑘 ∈
ω 𝑧 ∈ (𝐴 ↑𝑚
𝑘) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
70 | 58, 69 | sylbi 207 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
71 | 36, 70 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧))) |
72 | 71 | simpld 475 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → dom 𝑧 ∈ ω) |
73 | 10, 11, 12, 13 | fseqenlem1 8847 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑧 ∈ ω) → (𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1→𝐴) |
74 | 72, 73 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1→𝐴) |
75 | | f1f1orn 6148 |
. . . . . . . . 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 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧)) |
78 | | f1ocnvfv1 6532 |
. . . . . . . 8
⊢ (((𝐺‘dom 𝑧):(𝐴 ↑𝑚 dom 𝑧)–1-1-onto→ran
(𝐺‘dom 𝑧) ∧ 𝑧 ∈ (𝐴 ↑𝑚 dom 𝑧)) → (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧)) = 𝑧) |
79 | 76, 77, 78 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧)) = 𝑧) |
80 | 57, 79 | eqtr2d 2657 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤))) |
81 | 80 | ex 450 |
. . . . 5
⊢ (𝜑 → (𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)))) |
82 | 81 | alrimiv 1855 |
. . . 4
⊢ (𝜑 → ∀𝑧(𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)))) |
83 | | mo2icl 3385 |
. . . 4
⊢
(∀𝑧(𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤))) →
∃*𝑧 𝑧𝐾𝑤) |
84 | 82, 83 | syl 17 |
. . 3
⊢ (𝜑 → ∃*𝑧 𝑧𝐾𝑤) |
85 | 84 | alrimiv 1855 |
. 2
⊢ (𝜑 → ∀𝑤∃*𝑧 𝑧𝐾𝑤) |
86 | | dff12 6100 |
. 2
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)–1-1→(ω × 𝐴) ↔ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)⟶(ω ×
𝐴) ∧ ∀𝑤∃*𝑧 𝑧𝐾𝑤)) |
87 | 27, 85, 86 | sylanbrc 698 |
1
⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚
𝑘)–1-1→(ω × 𝐴)) |