Metamath Proof Explorer

Theorem infxpenc2lem2

Description: Lemma for infxpenc2 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc2.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
infxpenc2.2 ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
infxpenc2.3 ⊢ 𝑊 = ( ◡ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) )
infxpenc2.4 ⊢ ( 𝜑 → 𝐹 : ( ω ↑o 2o ) –1-1-onto→ ω )
infxpenc2.5 ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
infxpenc2.k ⊢ 𝐾 = ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) )
infxpenc2.h ⊢ 𝐻 = ( ( ( ω CNF 𝑊 ) ∘ 𝐾 ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) )
infxpenc2.l ⊢ 𝐿 = ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( 𝑌 ∘ ◡ 𝑋 ) ) ) )
infxpenc2.x ⊢ 𝑋 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) )
infxpenc2.y ⊢ 𝑌 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) )
infxpenc2.j ⊢ 𝐽 = ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ 𝐿 ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) )
infxpenc2.z ⊢ 𝑍 = ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) )
infxpenc2.t ⊢ 𝑇 = ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ⟨ ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑥 ) , ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑦 ) ⟩ )
infxpenc2.g ⊢ 𝐺 = ( ◡ ( 𝑛 ‘ 𝑏 ) ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) )
Assertion infxpenc2lem2 ( 𝜑 → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )

Proof

Step Hyp Ref Expression
1 infxpenc2.1 ⊢ ( 𝜑 → 𝐴 ∈ On )
2 infxpenc2.2 ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
3 infxpenc2.3 ⊢ 𝑊 = ( ◡ ( 𝑥 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑥 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) )
4 infxpenc2.4 ⊢ ( 𝜑 → 𝐹 : ( ω ↑o 2o ) –1-1-onto→ ω )
5 infxpenc2.5 ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
6 infxpenc2.k ⊢ 𝐾 = ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) )
7 infxpenc2.h ⊢ 𝐻 = ( ( ( ω CNF 𝑊 ) ∘ 𝐾 ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) )
8 infxpenc2.l ⊢ 𝐿 = ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( 𝑌 ∘ ◡ 𝑋 ) ) ) )
9 infxpenc2.x ⊢ 𝑋 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) )
10 infxpenc2.y ⊢ 𝑌 = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) )
11 infxpenc2.j ⊢ 𝐽 = ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ 𝐿 ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) )
12 infxpenc2.z ⊢ 𝑍 = ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) )
13 infxpenc2.t ⊢ 𝑇 = ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ⟨ ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑥 ) , ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑦 ) ⟩ )
14 infxpenc2.g ⊢ 𝐺 = ( ◡ ( 𝑛 ‘ 𝑏 ) ∘ ( ( ( 𝐻 ∘ 𝐽 ) ∘ 𝑍 ) ∘ 𝑇 ) )
15 1 mptexd ⊢ ( 𝜑 → ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ∈ V )
16 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝐴 ∈ On )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝑏 ∈ 𝐴 )
18 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ On )
19 16 17 18 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝑏 ∈ On )
20 simprr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ω ⊆ 𝑏 )
21 1 2 3 infxpenc2lem1 ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( 𝑊 ∈ ( On ∖ 1o ) ∧ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
22 21 simpld ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝑊 ∈ ( On ∖ 1o ) )
23 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝐹 : ( ω ↑o 2o ) –1-1-onto→ ω )
24 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( 𝐹 ‘ ∅ ) = ∅ )
25 21 simprd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) )
26 19 20 22 23 24 25 6 7 8 9 10 11 12 13 14 infxpenc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝐺 : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 )
27 f1of ⊢ ( 𝐺 : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 → 𝐺 : ( 𝑏 × 𝑏 ) ⟶ 𝑏 )
28 26 27 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝐺 : ( 𝑏 × 𝑏 ) ⟶ 𝑏 )
29 vex ⊢ 𝑏 ∈ V
30 29 29 xpex ⊢ ( 𝑏 × 𝑏 ) ∈ V
31 fex ⊢ ( ( 𝐺 : ( 𝑏 × 𝑏 ) ⟶ 𝑏 ∧ ( 𝑏 × 𝑏 ) ∈ V ) → 𝐺 ∈ V )
32 28 30 31 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → 𝐺 ∈ V )
33 eqid ⊢ ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) = ( 𝑏 ∈ 𝐴 ↦ 𝐺 )
34 33 fvmpt2 ⊢ ( ( 𝑏 ∈ 𝐴 ∧ 𝐺 ∈ V ) → ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) = 𝐺 )
35 17 32 34 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) = 𝐺 )
36 f1oeq1 ⊢ ( ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) = 𝐺 → ( ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ 𝐺 : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ 𝐺 : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
38 26 37 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) ) → ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 )
39 38 expr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ω ⊆ 𝑏 → ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
40 39 ralrimiva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
41 nfmpt1 ⊢ Ⅎ 𝑏 ( 𝑏 ∈ 𝐴 ↦ 𝐺 )
42 41 nfeq2 ⊢ Ⅎ 𝑏 𝑔 = ( 𝑏 ∈ 𝐴 ↦ 𝐺 )
43 fveq1 ⊢ ( 𝑔 = ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) → ( 𝑔 ‘ 𝑏 ) = ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) )
44 f1oeq1 ⊢ ( ( 𝑔 ‘ 𝑏 ) = ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) → ( ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
45 43 44 syl ⊢ ( 𝑔 = ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) → ( ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ↔ ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
46 45 imbi2d ⊢ ( 𝑔 = ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) → ( ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ↔ ( ω ⊆ 𝑏 → ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
47 42 46 ralbid ⊢ ( 𝑔 = ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) → ( ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( ( 𝑏 ∈ 𝐴 ↦ 𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
48 15 40 47 spcedv ⊢ ( 𝜑 → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )