Proof of Theorem infxpenc2lem2
Step | Hyp | Ref
| Expression |
1 | | infxpenc2.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ On) |
2 | 1 | mptexd 6761 |
. 2
⊢ (𝜑 → (𝑏 ∈ 𝐴 ↦ 𝐺) ∈ V) |
3 | 1 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐴 ∈ On) |
4 | | simprl 761 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ 𝐴) |
5 | | onelon 6003 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ On) |
6 | 3, 4, 5 | syl2anc 579 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑏 ∈ On) |
7 | | simprr 763 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ω ⊆ 𝑏) |
8 | | infxpenc2.2 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤))) |
9 | | infxpenc2.3 |
. . . . . . . 8
⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦
(ω ↑o 𝑥))‘ran (𝑛‘𝑏)) |
10 | 1, 8, 9 | infxpenc2lem1 9177 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1o) ∧
(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊))) |
11 | 10 | simpld 490 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝑊 ∈ (On ∖
1o)) |
12 | | infxpenc2.4 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(ω ↑o
2o)–1-1-onto→ω) |
13 | 12 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐹:(ω ↑o
2o)–1-1-onto→ω) |
14 | | infxpenc2.5 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘∅) = ∅) |
15 | 14 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝐹‘∅) = ∅) |
16 | 10 | simprd 491 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)) |
17 | | infxpenc2.k |
. . . . . 6
⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o
2o) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) |
18 | | infxpenc2.h |
. . . . . 6
⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o)
CNF 𝑊)) |
19 | | infxpenc2.l |
. . . . . 6
⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚
(𝑊 ·o
2o)) ∣ 𝑥
finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋)))) |
20 | | infxpenc2.x |
. . . . . 6
⊢ 𝑋 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤)) |
21 | | infxpenc2.y |
. . . . . 6
⊢ 𝑌 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((2o
·o 𝑤)
+o 𝑧)) |
22 | | infxpenc2.j |
. . . . . 6
⊢ 𝐽 = (((ω CNF (2o
·o 𝑊))
∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·o
2o))) |
23 | | infxpenc2.z |
. . . . . 6
⊢ 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω
↑o 𝑊)
·o 𝑥)
+o 𝑦)) |
24 | | infxpenc2.t |
. . . . . 6
⊢ 𝑇 = (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ 〈((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)〉) |
25 | | infxpenc2.g |
. . . . . 6
⊢ 𝐺 = (◡(𝑛‘𝑏) ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇)) |
26 | 6, 7, 11, 13, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25 | infxpenc 9176 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏) |
27 | | f1of 6393 |
. . . . . . . . 9
⊢ (𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏 → 𝐺:(𝑏 × 𝑏)⟶𝑏) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺:(𝑏 × 𝑏)⟶𝑏) |
29 | | vex 3401 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
30 | 29, 29 | xpex 7242 |
. . . . . . . 8
⊢ (𝑏 × 𝑏) ∈ V |
31 | | fex 6763 |
. . . . . . . 8
⊢ ((𝐺:(𝑏 × 𝑏)⟶𝑏 ∧ (𝑏 × 𝑏) ∈ V) → 𝐺 ∈ V) |
32 | 28, 30, 31 | sylancl 580 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → 𝐺 ∈ V) |
33 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐴 ↦ 𝐺) = (𝑏 ∈ 𝐴 ↦ 𝐺) |
34 | 33 | fvmpt2 6554 |
. . . . . . 7
⊢ ((𝑏 ∈ 𝐴 ∧ 𝐺 ∈ V) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺) |
35 | 4, 32, 34 | syl2anc 579 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺) |
36 | | f1oeq1 6382 |
. . . . . 6
⊢ (((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) = 𝐺 → (((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏)) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ 𝐺:(𝑏 × 𝑏)–1-1-onto→𝑏)) |
38 | 26, 37 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) |
39 | 38 | expr 450 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
40 | 39 | ralrimiva 3148 |
. 2
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
41 | | nfmpt1 4984 |
. . . 4
⊢
Ⅎ𝑏(𝑏 ∈ 𝐴 ↦ 𝐺) |
42 | 41 | nfeq2 2949 |
. . 3
⊢
Ⅎ𝑏 𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) |
43 | | fveq1 6447 |
. . . . 5
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → (𝑔‘𝑏) = ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏)) |
44 | | f1oeq1 6382 |
. . . . 5
⊢ ((𝑔‘𝑏) = ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏) → ((𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
45 | 43, 44 | syl 17 |
. . . 4
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → ((𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏 ↔ ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |
46 | 45 | imbi2d 332 |
. . 3
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → ((ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
47 | 42, 46 | ralbid 3165 |
. 2
⊢ (𝑔 = (𝑏 ∈ 𝐴 ↦ 𝐺) → (∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏) ↔ ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ((𝑏 ∈ 𝐴 ↦ 𝐺)‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))) |
48 | 2, 40, 47 | elabd 3560 |
1
⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏)) |