Step | Hyp | Ref
| Expression |
1 | | cnfcom.1 |
. 2
⊢ (𝜑 → 𝐼 ∈ dom 𝐺) |
2 | | cnfcom.s |
. . . . . 6
⊢ 𝑆 = dom (ω CNF 𝐴) |
3 | | omelon 9266 |
. . . . . . 7
⊢ ω
∈ On |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ω ∈
On) |
5 | | cnfcom.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ On) |
6 | | cnfcom.g |
. . . . . 6
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
7 | | cnfcom.f |
. . . . . . 7
⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵) |
8 | 2, 4, 5 | cantnff1o 9316 |
. . . . . . . . 9
⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴)) |
9 | | f1ocnv 6678 |
. . . . . . . . 9
⊢ ((ω
CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆) |
10 | | f1of 6666 |
. . . . . . . . 9
⊢ (◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆) |
12 | | cnfcom.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴)) |
13 | 11, 12 | ffvelrnd 6910 |
. . . . . . 7
⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆) |
14 | 7, 13 | eqeltrid 2842 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
15 | 2, 4, 5, 6, 14 | cantnfcl 9287 |
. . . . 5
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) |
16 | 15 | simprd 499 |
. . . 4
⊢ (𝜑 → dom 𝐺 ∈ ω) |
17 | | elnn 7660 |
. . . 4
⊢ ((𝐼 ∈ dom 𝐺 ∧ dom 𝐺 ∈ ω) → 𝐼 ∈ ω) |
18 | 1, 16, 17 | syl2anc 587 |
. . 3
⊢ (𝜑 → 𝐼 ∈ ω) |
19 | | eleq1 2825 |
. . . . . 6
⊢ (𝑤 = 𝐼 → (𝑤 ∈ dom 𝐺 ↔ 𝐼 ∈ dom 𝐺)) |
20 | | suceq 6283 |
. . . . . . . 8
⊢ (𝑤 = 𝐼 → suc 𝑤 = suc 𝐼) |
21 | 20 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = 𝐼 → (𝑇‘suc 𝑤) = (𝑇‘suc 𝐼)) |
22 | 20 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = 𝐼 → (𝐻‘suc 𝑤) = (𝐻‘suc 𝐼)) |
23 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑤 = 𝐼 → (𝐺‘𝑤) = (𝐺‘𝐼)) |
24 | 23 | oveq2d 7234 |
. . . . . . . 8
⊢ (𝑤 = 𝐼 → (ω ↑o (𝐺‘𝑤)) = (ω ↑o (𝐺‘𝐼))) |
25 | | 2fveq3 6727 |
. . . . . . . 8
⊢ (𝑤 = 𝐼 → (𝐹‘(𝐺‘𝑤)) = (𝐹‘(𝐺‘𝐼))) |
26 | 24, 25 | oveq12d 7236 |
. . . . . . 7
⊢ (𝑤 = 𝐼 → ((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) = ((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) |
27 | 21, 22, 26 | f1oeq123d 6660 |
. . . . . 6
⊢ (𝑤 = 𝐼 → ((𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) ↔ (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))) |
28 | 19, 27 | imbi12d 348 |
. . . . 5
⊢ (𝑤 = 𝐼 → ((𝑤 ∈ dom 𝐺 → (𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤)))) ↔ (𝐼 ∈ dom 𝐺 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))) |
29 | 28 | imbi2d 344 |
. . . 4
⊢ (𝑤 = 𝐼 → ((𝜑 → (𝑤 ∈ dom 𝐺 → (𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))))) ↔ (𝜑 → (𝐼 ∈ dom 𝐺 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))))) |
30 | | eleq1 2825 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝑤 ∈ dom 𝐺 ↔ ∅ ∈ dom 𝐺)) |
31 | | suceq 6283 |
. . . . . . . 8
⊢ (𝑤 = ∅ → suc 𝑤 = suc ∅) |
32 | 31 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝑇‘suc 𝑤) = (𝑇‘suc ∅)) |
33 | 31 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝐻‘suc 𝑤) = (𝐻‘suc ∅)) |
34 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝐺‘𝑤) = (𝐺‘∅)) |
35 | 34 | oveq2d 7234 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (ω
↑o (𝐺‘𝑤)) = (ω ↑o (𝐺‘∅))) |
36 | | 2fveq3 6727 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (𝐹‘(𝐺‘𝑤)) = (𝐹‘(𝐺‘∅))) |
37 | 35, 36 | oveq12d 7236 |
. . . . . . 7
⊢ (𝑤 = ∅ → ((ω
↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) = ((ω ↑o (𝐺‘∅))
·o (𝐹‘(𝐺‘∅)))) |
38 | 32, 33, 37 | f1oeq123d 6660 |
. . . . . 6
⊢ (𝑤 = ∅ → ((𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) ↔ (𝑇‘suc ∅):(𝐻‘suc ∅)–1-1-onto→((ω ↑o (𝐺‘∅))
·o (𝐹‘(𝐺‘∅))))) |
39 | 30, 38 | imbi12d 348 |
. . . . 5
⊢ (𝑤 = ∅ → ((𝑤 ∈ dom 𝐺 → (𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤)))) ↔ (∅ ∈ dom 𝐺 → (𝑇‘suc ∅):(𝐻‘suc ∅)–1-1-onto→((ω ↑o (𝐺‘∅))
·o (𝐹‘(𝐺‘∅)))))) |
40 | | eleq1 2825 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (𝑤 ∈ dom 𝐺 ↔ 𝑦 ∈ dom 𝐺)) |
41 | | suceq 6283 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → suc 𝑤 = suc 𝑦) |
42 | 41 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑇‘suc 𝑤) = (𝑇‘suc 𝑦)) |
43 | 41 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝐻‘suc 𝑤) = (𝐻‘suc 𝑦)) |
44 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑤 = 𝑦 → (𝐺‘𝑤) = (𝐺‘𝑦)) |
45 | 44 | oveq2d 7234 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (ω ↑o (𝐺‘𝑤)) = (ω ↑o (𝐺‘𝑦))) |
46 | | 2fveq3 6727 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → (𝐹‘(𝐺‘𝑤)) = (𝐹‘(𝐺‘𝑦))) |
47 | 45, 46 | oveq12d 7236 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → ((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) = ((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦)))) |
48 | 42, 43, 47 | f1oeq123d 6660 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) ↔ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) |
49 | 40, 48 | imbi12d 348 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((𝑤 ∈ dom 𝐺 → (𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤)))) ↔ (𝑦 ∈ dom 𝐺 → (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦)))))) |
50 | | eleq1 2825 |
. . . . . 6
⊢ (𝑤 = suc 𝑦 → (𝑤 ∈ dom 𝐺 ↔ suc 𝑦 ∈ dom 𝐺)) |
51 | | suceq 6283 |
. . . . . . . 8
⊢ (𝑤 = suc 𝑦 → suc 𝑤 = suc suc 𝑦) |
52 | 51 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = suc 𝑦 → (𝑇‘suc 𝑤) = (𝑇‘suc suc 𝑦)) |
53 | 51 | fveq2d 6726 |
. . . . . . 7
⊢ (𝑤 = suc 𝑦 → (𝐻‘suc 𝑤) = (𝐻‘suc suc 𝑦)) |
54 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑤 = suc 𝑦 → (𝐺‘𝑤) = (𝐺‘suc 𝑦)) |
55 | 54 | oveq2d 7234 |
. . . . . . . 8
⊢ (𝑤 = suc 𝑦 → (ω ↑o (𝐺‘𝑤)) = (ω ↑o (𝐺‘suc 𝑦))) |
56 | | 2fveq3 6727 |
. . . . . . . 8
⊢ (𝑤 = suc 𝑦 → (𝐹‘(𝐺‘𝑤)) = (𝐹‘(𝐺‘suc 𝑦))) |
57 | 55, 56 | oveq12d 7236 |
. . . . . . 7
⊢ (𝑤 = suc 𝑦 → ((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) = ((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦)))) |
58 | 52, 53, 57 | f1oeq123d 6660 |
. . . . . 6
⊢ (𝑤 = suc 𝑦 → ((𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤))) ↔ (𝑇‘suc suc 𝑦):(𝐻‘suc suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))))) |
59 | 50, 58 | imbi12d 348 |
. . . . 5
⊢ (𝑤 = suc 𝑦 → ((𝑤 ∈ dom 𝐺 → (𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤)))) ↔ (suc 𝑦 ∈ dom 𝐺 → (𝑇‘suc suc 𝑦):(𝐻‘suc suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦)))))) |
60 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐴 ∈ On) |
61 | 12 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → 𝐵 ∈ (ω ↑o 𝐴)) |
62 | | cnfcom.h |
. . . . . . 7
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅) |
63 | | cnfcom.t |
. . . . . . 7
⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅) |
64 | | cnfcom.m |
. . . . . . 7
⊢ 𝑀 = ((ω ↑o
(𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) |
65 | | cnfcom.k |
. . . . . . 7
⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥))) |
66 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ dom
𝐺) |
67 | 3 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ω ∈
On) |
68 | | suppssdm 7924 |
. . . . . . . . . . 11
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
69 | 2, 4, 5 | cantnfs 9286 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))) |
70 | 14, 69 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)) |
71 | 70 | simpld 498 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ω) |
72 | 68, 71 | fssdm 6570 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐴) |
73 | | onss 7573 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
74 | 5, 73 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ On) |
75 | 72, 74 | sstrd 3916 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 supp ∅) ⊆ On) |
76 | 6 | oif 9151 |
. . . . . . . . . 10
⊢ 𝐺:dom 𝐺⟶(𝐹 supp ∅) |
77 | 76 | ffvelrni 6908 |
. . . . . . . . 9
⊢ (∅
∈ dom 𝐺 → (𝐺‘∅) ∈ (𝐹 supp ∅)) |
78 | | ssel2 3900 |
. . . . . . . . 9
⊢ (((𝐹 supp ∅) ⊆ On ∧
(𝐺‘∅) ∈
(𝐹 supp ∅)) →
(𝐺‘∅) ∈
On) |
79 | 75, 77, 78 | syl2an 599 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝐺‘∅) ∈ On) |
80 | | peano1 7672 |
. . . . . . . . 9
⊢ ∅
∈ ω |
81 | 80 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈
ω) |
82 | | oen0 8319 |
. . . . . . . 8
⊢
(((ω ∈ On ∧ (𝐺‘∅) ∈ On) ∧ ∅
∈ ω) → ∅ ∈ (ω ↑o (𝐺‘∅))) |
83 | 67, 79, 81, 82 | syl21anc 838 |
. . . . . . 7
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → ∅ ∈ (ω
↑o (𝐺‘∅))) |
84 | | 0ex 5205 |
. . . . . . . . 9
⊢ ∅
∈ V |
85 | 63 | seqom0g 8197 |
. . . . . . . . 9
⊢ (∅
∈ V → (𝑇‘∅) = ∅) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑇‘∅) =
∅ |
87 | | f1o0 6702 |
. . . . . . . . . 10
⊢
∅:∅–1-1-onto→∅ |
88 | 62 | seqom0g 8197 |
. . . . . . . . . . 11
⊢ (∅
∈ V → (𝐻‘∅) = ∅) |
89 | | f1oeq2 6655 |
. . . . . . . . . . 11
⊢ ((𝐻‘∅) = ∅ →
(∅:(𝐻‘∅)–1-1-onto→∅ ↔ ∅:∅–1-1-onto→∅)) |
90 | 84, 88, 89 | mp2b 10 |
. . . . . . . . . 10
⊢
(∅:(𝐻‘∅)–1-1-onto→∅ ↔ ∅:∅–1-1-onto→∅) |
91 | 87, 90 | mpbir 234 |
. . . . . . . . 9
⊢
∅:(𝐻‘∅)–1-1-onto→∅ |
92 | | f1oeq1 6654 |
. . . . . . . . 9
⊢ ((𝑇‘∅) = ∅ →
((𝑇‘∅):(𝐻‘∅)–1-1-onto→∅ ↔ ∅:(𝐻‘∅)–1-1-onto→∅)) |
93 | 91, 92 | mpbiri 261 |
. . . . . . . 8
⊢ ((𝑇‘∅) = ∅ →
(𝑇‘∅):(𝐻‘∅)–1-1-onto→∅) |
94 | 86, 93 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝑇‘∅):(𝐻‘∅)–1-1-onto→∅) |
95 | 2, 60, 61, 7, 6, 62, 63, 64, 65, 66, 83, 94 | cnfcomlem 9319 |
. . . . . 6
⊢ ((𝜑 ∧ ∅ ∈ dom 𝐺) → (𝑇‘suc ∅):(𝐻‘suc ∅)–1-1-onto→((ω ↑o (𝐺‘∅))
·o (𝐹‘(𝐺‘∅)))) |
96 | 95 | ex 416 |
. . . . 5
⊢ (𝜑 → (∅ ∈ dom 𝐺 → (𝑇‘suc ∅):(𝐻‘suc ∅)–1-1-onto→((ω ↑o (𝐺‘∅))
·o (𝐹‘(𝐺‘∅))))) |
97 | 6 | oicl 9150 |
. . . . . . . . . 10
⊢ Ord dom
𝐺 |
98 | | ordtr 6232 |
. . . . . . . . . 10
⊢ (Ord dom
𝐺 → Tr dom 𝐺) |
99 | 97, 98 | ax-mp 5 |
. . . . . . . . 9
⊢ Tr dom
𝐺 |
100 | | trsuc 6302 |
. . . . . . . . 9
⊢ ((Tr dom
𝐺 ∧ suc 𝑦 ∈ dom 𝐺) → 𝑦 ∈ dom 𝐺) |
101 | 99, 100 | mpan 690 |
. . . . . . . 8
⊢ (suc
𝑦 ∈ dom 𝐺 → 𝑦 ∈ dom 𝐺) |
102 | 101 | imim1i 63 |
. . . . . . 7
⊢ ((𝑦 ∈ dom 𝐺 → (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦)))) → (suc 𝑦 ∈ dom 𝐺 → (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) |
103 | 5 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → 𝐴 ∈ On) |
104 | 12 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → 𝐵 ∈ (ω ↑o 𝐴)) |
105 | | simprl 771 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → suc 𝑦 ∈ dom 𝐺) |
106 | 74 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → 𝐴 ⊆ On) |
107 | 72 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐹 supp ∅) ⊆ 𝐴) |
108 | 76 | ffvelrni 6908 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝑦 ∈ dom 𝐺 → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅)) |
109 | 108 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐺‘suc 𝑦) ∈ (𝐹 supp ∅)) |
110 | 107, 109 | sseldd 3907 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐺‘suc 𝑦) ∈ 𝐴) |
111 | 106, 110 | sseldd 3907 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐺‘suc 𝑦) ∈ On) |
112 | | eloni 6228 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘suc 𝑦) ∈ On → Ord (𝐺‘suc 𝑦)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → Ord (𝐺‘suc 𝑦)) |
114 | | vex 3417 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ V |
115 | 114 | sucid 6297 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ suc 𝑦 |
116 | | ovexd 7253 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) |
117 | 15 | simpld 498 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → E We (𝐹 supp ∅)) |
118 | 6 | oiiso 9158 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
119 | 116, 117,
118 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
120 | 119 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → 𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅))) |
121 | 101 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → 𝑦 ∈ dom 𝐺) |
122 | | isorel 7140 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 Isom E , E (dom 𝐺, (𝐹 supp ∅)) ∧ (𝑦 ∈ dom 𝐺 ∧ suc 𝑦 ∈ dom 𝐺)) → (𝑦 E suc 𝑦 ↔ (𝐺‘𝑦) E (𝐺‘suc 𝑦))) |
123 | 120, 121,
105, 122 | syl12anc 837 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝑦 E suc 𝑦 ↔ (𝐺‘𝑦) E (𝐺‘suc 𝑦))) |
124 | 114 | sucex 7595 |
. . . . . . . . . . . . . . . 16
⊢ suc 𝑦 ∈ V |
125 | 124 | epeli 5467 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 E suc 𝑦 ↔ 𝑦 ∈ suc 𝑦) |
126 | | fvex 6735 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺‘suc 𝑦) ∈ V |
127 | 126 | epeli 5467 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺‘𝑦) E (𝐺‘suc 𝑦) ↔ (𝐺‘𝑦) ∈ (𝐺‘suc 𝑦)) |
128 | 123, 125,
127 | 3bitr3g 316 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝑦 ∈ suc 𝑦 ↔ (𝐺‘𝑦) ∈ (𝐺‘suc 𝑦))) |
129 | 115, 128 | mpbii 236 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐺‘𝑦) ∈ (𝐺‘suc 𝑦)) |
130 | | ordsucss 7602 |
. . . . . . . . . . . . 13
⊢ (Ord
(𝐺‘suc 𝑦) → ((𝐺‘𝑦) ∈ (𝐺‘suc 𝑦) → suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦))) |
131 | 113, 129,
130 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦)) |
132 | 76 | ffvelrni 6908 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ dom 𝐺 → (𝐺‘𝑦) ∈ (𝐹 supp ∅)) |
133 | 121, 132 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐺‘𝑦) ∈ (𝐹 supp ∅)) |
134 | 107, 133 | sseldd 3907 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐺‘𝑦) ∈ 𝐴) |
135 | 106, 134 | sseldd 3907 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐺‘𝑦) ∈ On) |
136 | | suceloni 7597 |
. . . . . . . . . . . . . 14
⊢ ((𝐺‘𝑦) ∈ On → suc (𝐺‘𝑦) ∈ On) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → suc (𝐺‘𝑦) ∈ On) |
138 | 3 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → ω ∈
On) |
139 | 80 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → ∅ ∈
ω) |
140 | | oewordi 8324 |
. . . . . . . . . . . . 13
⊢ (((suc
(𝐺‘𝑦) ∈ On ∧ (𝐺‘suc 𝑦) ∈ On ∧ ω ∈ On) ∧
∅ ∈ ω) → (suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → (ω ↑o suc
(𝐺‘𝑦)) ⊆ (ω ↑o (𝐺‘suc 𝑦)))) |
141 | 137, 111,
138, 139, 140 | syl31anc 1375 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (suc (𝐺‘𝑦) ⊆ (𝐺‘suc 𝑦) → (ω ↑o suc
(𝐺‘𝑦)) ⊆ (ω ↑o (𝐺‘suc 𝑦)))) |
142 | 131, 141 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (ω ↑o suc
(𝐺‘𝑦)) ⊆ (ω ↑o (𝐺‘suc 𝑦))) |
143 | 71 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → 𝐹:𝐴⟶ω) |
144 | 143, 134 | ffvelrnd 6910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐹‘(𝐺‘𝑦)) ∈ ω) |
145 | | nnon 7655 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘(𝐺‘𝑦)) ∈ ω → (𝐹‘(𝐺‘𝑦)) ∈ On) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝐹‘(𝐺‘𝑦)) ∈ On) |
147 | | oecl 8269 |
. . . . . . . . . . . . . . 15
⊢ ((ω
∈ On ∧ (𝐺‘𝑦) ∈ On) → (ω
↑o (𝐺‘𝑦)) ∈ On) |
148 | 138, 135,
147 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (ω ↑o
(𝐺‘𝑦)) ∈ On) |
149 | | oen0 8319 |
. . . . . . . . . . . . . . 15
⊢
(((ω ∈ On ∧ (𝐺‘𝑦) ∈ On) ∧ ∅ ∈ ω)
→ ∅ ∈ (ω ↑o (𝐺‘𝑦))) |
150 | 138, 135,
139, 149 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → ∅ ∈ (ω
↑o (𝐺‘𝑦))) |
151 | | omord2 8300 |
. . . . . . . . . . . . . 14
⊢ ((((𝐹‘(𝐺‘𝑦)) ∈ On ∧ ω ∈ On ∧
(ω ↑o (𝐺‘𝑦)) ∈ On) ∧ ∅ ∈ (ω
↑o (𝐺‘𝑦))) → ((𝐹‘(𝐺‘𝑦)) ∈ ω ↔ ((ω
↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ ((ω ↑o
(𝐺‘𝑦)) ·o
ω))) |
152 | 146, 138,
148, 150, 151 | syl31anc 1375 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → ((𝐹‘(𝐺‘𝑦)) ∈ ω ↔ ((ω
↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ ((ω ↑o
(𝐺‘𝑦)) ·o
ω))) |
153 | 144, 152 | mpbid 235 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → ((ω ↑o
(𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ ((ω ↑o
(𝐺‘𝑦)) ·o
ω)) |
154 | | oesuc 8259 |
. . . . . . . . . . . . 13
⊢ ((ω
∈ On ∧ (𝐺‘𝑦) ∈ On) → (ω
↑o suc (𝐺‘𝑦)) = ((ω ↑o (𝐺‘𝑦)) ·o
ω)) |
155 | 138, 135,
154 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (ω ↑o suc
(𝐺‘𝑦)) = ((ω ↑o (𝐺‘𝑦)) ·o
ω)) |
156 | 153, 155 | eleqtrrd 2841 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → ((ω ↑o
(𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ (ω ↑o suc
(𝐺‘𝑦))) |
157 | 142, 156 | sseldd 3907 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → ((ω ↑o
(𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) ∈ (ω ↑o (𝐺‘suc 𝑦))) |
158 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦)))) |
159 | 2, 103, 104, 7, 6, 62, 63, 64, 65, 105, 157, 158 | cnfcomlem 9319 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ω) ∧ (suc 𝑦 ∈ dom 𝐺 ∧ (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))))) → (𝑇‘suc suc 𝑦):(𝐻‘suc suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦)))) |
160 | 159 | exp32 424 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (suc 𝑦 ∈ dom 𝐺 → ((𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦))) → (𝑇‘suc suc 𝑦):(𝐻‘suc suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦)))))) |
161 | 160 | a2d 29 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((suc 𝑦 ∈ dom 𝐺 → (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦)))) → (suc 𝑦 ∈ dom 𝐺 → (𝑇‘suc suc 𝑦):(𝐻‘suc suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦)))))) |
162 | 102, 161 | syl5 34 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → ((𝑦 ∈ dom 𝐺 → (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦)))) → (suc 𝑦 ∈ dom 𝐺 → (𝑇‘suc suc 𝑦):(𝐻‘suc suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦)))))) |
163 | 162 | expcom 417 |
. . . . 5
⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝐺 → (𝑇‘suc 𝑦):(𝐻‘suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘𝑦)) ·o (𝐹‘(𝐺‘𝑦)))) → (suc 𝑦 ∈ dom 𝐺 → (𝑇‘suc suc 𝑦):(𝐻‘suc suc 𝑦)–1-1-onto→((ω ↑o (𝐺‘suc 𝑦)) ·o (𝐹‘(𝐺‘suc 𝑦))))))) |
164 | 39, 49, 59, 96, 163 | finds2 7683 |
. . . 4
⊢ (𝑤 ∈ ω → (𝜑 → (𝑤 ∈ dom 𝐺 → (𝑇‘suc 𝑤):(𝐻‘suc 𝑤)–1-1-onto→((ω ↑o (𝐺‘𝑤)) ·o (𝐹‘(𝐺‘𝑤)))))) |
165 | 29, 164 | vtoclga 3494 |
. . 3
⊢ (𝐼 ∈ ω → (𝜑 → (𝐼 ∈ dom 𝐺 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))))) |
166 | 18, 165 | mpcom 38 |
. 2
⊢ (𝜑 → (𝐼 ∈ dom 𝐺 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼))))) |
167 | 1, 166 | mpd 15 |
1
⊢ (𝜑 → (𝑇‘suc 𝐼):(𝐻‘suc 𝐼)–1-1-onto→((ω ↑o (𝐺‘𝐼)) ·o (𝐹‘(𝐺‘𝐼)))) |