| Step | Hyp | Ref
| Expression |
| 1 | | eliun 4995 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) ↔ ∃𝑘 ∈ ω 𝑦 ∈ (𝐴 ↑m 𝑘)) |
| 2 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴 ↑m 𝑘) → 𝑦:𝑘⟶𝐴) |
| 3 | 2 | ad2antll 729 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → 𝑦:𝑘⟶𝐴) |
| 4 | 3 | fdmd 6746 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → dom 𝑦 = 𝑘) |
| 5 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → 𝑘 ∈ ω) |
| 6 | 4, 5 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → dom 𝑦 ∈ ω) |
| 7 | 4 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → (𝐺‘dom 𝑦) = (𝐺‘𝑘)) |
| 8 | 7 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → ((𝐺‘dom 𝑦)‘𝑦) = ((𝐺‘𝑘)‘𝑦)) |
| 9 | | fseqenlem.a |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 10 | | fseqenlem.b |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
| 11 | | fseqenlem.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) |
| 12 | | fseqenlem.g |
. . . . . . . . . . . 12
⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) |
| 13 | 9, 10, 11, 12 | fseqenlem1 10064 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ω) → (𝐺‘𝑘):(𝐴 ↑m 𝑘)–1-1→𝐴) |
| 14 | 13 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → (𝐺‘𝑘):(𝐴 ↑m 𝑘)–1-1→𝐴) |
| 15 | | f1f 6804 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑘):(𝐴 ↑m 𝑘)–1-1→𝐴 → (𝐺‘𝑘):(𝐴 ↑m 𝑘)⟶𝐴) |
| 16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → (𝐺‘𝑘):(𝐴 ↑m 𝑘)⟶𝐴) |
| 17 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → 𝑦 ∈ (𝐴 ↑m 𝑘)) |
| 18 | 16, 17 | ffvelcdmd 7105 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → ((𝐺‘𝑘)‘𝑦) ∈ 𝐴) |
| 19 | 8, 18 | eqeltrd 2841 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → ((𝐺‘dom 𝑦)‘𝑦) ∈ 𝐴) |
| 20 | 6, 19 | opelxpd 5724 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑘 ∈ ω ∧ 𝑦 ∈ (𝐴 ↑m 𝑘))) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
| 21 | 20 | rexlimdvaa 3156 |
. . . . 5
⊢ (𝜑 → (∃𝑘 ∈ ω 𝑦 ∈ (𝐴 ↑m 𝑘) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴))) |
| 22 | 1, 21 | biimtrid 242 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑m 𝑘) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴))) |
| 23 | 22 | imp 406 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑m 𝑘)) → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 ∈ (ω × 𝐴)) |
| 24 | | fseqenlem.k |
. . 3
⊢ 𝐾 = (𝑦 ∈ ∪
𝑘 ∈ ω (𝐴 ↑m 𝑘) ↦ 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉) |
| 25 | 23, 24 | fmptd 7134 |
. 2
⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)⟶(ω × 𝐴)) |
| 26 | | ffun 6739 |
. . . . . . . . . . . . . . 15
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)⟶(ω × 𝐴) → Fun 𝐾) |
| 27 | | funbrfv2b 6966 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝐾 → (𝑧𝐾𝑤 ↔ (𝑧 ∈ dom 𝐾 ∧ (𝐾‘𝑧) = 𝑤))) |
| 28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑧𝐾𝑤 ↔ (𝑧 ∈ dom 𝐾 ∧ (𝐾‘𝑧) = 𝑤))) |
| 29 | 28 | simplbda 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐾‘𝑧) = 𝑤) |
| 30 | 28 | simprbda 498 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ dom 𝐾) |
| 31 | 25 | fdmd 6746 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → dom 𝐾 = ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)) |
| 33 | 30, 32 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ ∪
𝑘 ∈ ω (𝐴 ↑m 𝑘)) |
| 34 | | dmeq 5914 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → dom 𝑦 = dom 𝑧) |
| 35 | 34 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (𝐺‘dom 𝑦) = (𝐺‘dom 𝑧)) |
| 36 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
| 37 | 35, 36 | fveq12d 6913 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → ((𝐺‘dom 𝑦)‘𝑦) = ((𝐺‘dom 𝑧)‘𝑧)) |
| 38 | 34, 37 | opeq12d 4881 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉 = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
| 39 | | opex 5469 |
. . . . . . . . . . . . . . 15
⊢ 〈dom
𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉 ∈ V |
| 40 | 38, 24, 39 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) → (𝐾‘𝑧) = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
| 41 | 33, 40 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐾‘𝑧) = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
| 42 | 29, 41 | eqtr3d 2779 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑤 = 〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) |
| 43 | 42 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (1st ‘𝑤) = (1st
‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉)) |
| 44 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
| 45 | 44 | dmex 7931 |
. . . . . . . . . . . 12
⊢ dom 𝑧 ∈ V |
| 46 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ ((𝐺‘dom 𝑧)‘𝑧) ∈ V |
| 47 | 45, 46 | op1st 8022 |
. . . . . . . . . . 11
⊢
(1st ‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) = dom 𝑧 |
| 48 | 43, 47 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (1st ‘𝑤) = dom 𝑧) |
| 49 | 48 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘(1st ‘𝑤)) = (𝐺‘dom 𝑧)) |
| 50 | 49 | cnveqd 5886 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → ◡(𝐺‘(1st ‘𝑤)) = ◡(𝐺‘dom 𝑧)) |
| 51 | 42 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (2nd ‘𝑤) = (2nd
‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉)) |
| 52 | 45, 46 | op2nd 8023 |
. . . . . . . . 9
⊢
(2nd ‘〈dom 𝑧, ((𝐺‘dom 𝑧)‘𝑧)〉) = ((𝐺‘dom 𝑧)‘𝑧) |
| 53 | 51, 52 | eqtrdi 2793 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (2nd ‘𝑤) = ((𝐺‘dom 𝑧)‘𝑧)) |
| 54 | 50, 53 | fveq12d 6913 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)) = (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧))) |
| 55 | | eliun 4995 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) ↔ ∃𝑘 ∈ ω 𝑧 ∈ (𝐴 ↑m 𝑘)) |
| 56 | | elmapi 8889 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ (𝐴 ↑m 𝑘) → 𝑧:𝑘⟶𝐴) |
| 57 | 56 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → 𝑧:𝑘⟶𝐴) |
| 58 | 57 | fdmd 6746 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → dom 𝑧 = 𝑘) |
| 59 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → 𝑘 ∈ ω) |
| 60 | 58, 59 | eqeltrd 2841 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → dom 𝑧 ∈ ω) |
| 61 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → 𝑧 ∈ (𝐴 ↑m 𝑘)) |
| 62 | 58 | oveq2d 7447 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → (𝐴 ↑m dom 𝑧) = (𝐴 ↑m 𝑘)) |
| 63 | 61, 62 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → 𝑧 ∈ (𝐴 ↑m dom 𝑧)) |
| 64 | 60, 63 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m 𝑘)) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m dom 𝑧))) |
| 65 | 64 | rexlimiva 3147 |
. . . . . . . . . . . . 13
⊢
(∃𝑘 ∈
ω 𝑧 ∈ (𝐴 ↑m 𝑘) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m dom 𝑧))) |
| 66 | 55, 65 | sylbi 217 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m dom 𝑧))) |
| 67 | 33, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (dom 𝑧 ∈ ω ∧ 𝑧 ∈ (𝐴 ↑m dom 𝑧))) |
| 68 | 67 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → dom 𝑧 ∈ ω) |
| 69 | 9, 10, 11, 12 | fseqenlem1 10064 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ dom 𝑧 ∈ ω) → (𝐺‘dom 𝑧):(𝐴 ↑m dom 𝑧)–1-1→𝐴) |
| 70 | 68, 69 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘dom 𝑧):(𝐴 ↑m dom 𝑧)–1-1→𝐴) |
| 71 | | f1f1orn 6859 |
. . . . . . . . 9
⊢ ((𝐺‘dom 𝑧):(𝐴 ↑m dom 𝑧)–1-1→𝐴 → (𝐺‘dom 𝑧):(𝐴 ↑m dom 𝑧)–1-1-onto→ran
(𝐺‘dom 𝑧)) |
| 72 | 70, 71 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (𝐺‘dom 𝑧):(𝐴 ↑m dom 𝑧)–1-1-onto→ran
(𝐺‘dom 𝑧)) |
| 73 | 67 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 ∈ (𝐴 ↑m dom 𝑧)) |
| 74 | | f1ocnvfv1 7296 |
. . . . . . . 8
⊢ (((𝐺‘dom 𝑧):(𝐴 ↑m dom 𝑧)–1-1-onto→ran
(𝐺‘dom 𝑧) ∧ 𝑧 ∈ (𝐴 ↑m dom 𝑧)) → (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧)) = 𝑧) |
| 75 | 72, 73, 74 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → (◡(𝐺‘dom 𝑧)‘((𝐺‘dom 𝑧)‘𝑧)) = 𝑧) |
| 76 | 54, 75 | eqtr2d 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧𝐾𝑤) → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤))) |
| 77 | 76 | ex 412 |
. . . . 5
⊢ (𝜑 → (𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)))) |
| 78 | 77 | alrimiv 1927 |
. . . 4
⊢ (𝜑 → ∀𝑧(𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤)))) |
| 79 | | mo2icl 3720 |
. . . 4
⊢
(∀𝑧(𝑧𝐾𝑤 → 𝑧 = (◡(𝐺‘(1st ‘𝑤))‘(2nd
‘𝑤))) →
∃*𝑧 𝑧𝐾𝑤) |
| 80 | 78, 79 | syl 17 |
. . 3
⊢ (𝜑 → ∃*𝑧 𝑧𝐾𝑤) |
| 81 | 80 | alrimiv 1927 |
. 2
⊢ (𝜑 → ∀𝑤∃*𝑧 𝑧𝐾𝑤) |
| 82 | | dff12 6803 |
. 2
⊢ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)–1-1→(ω × 𝐴) ↔ (𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)⟶(ω × 𝐴) ∧ ∀𝑤∃*𝑧 𝑧𝐾𝑤)) |
| 83 | 25, 81, 82 | sylanbrc 583 |
1
⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)–1-1→(ω × 𝐴)) |