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 35 f1oeq1d ( ( 𝜑 ∧ ( 𝑏𝐴 ∧ ω ⊆ 𝑏 ) ) → ( ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏𝐺 : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) )
37 26 36 mpbird ( ( 𝜑 ∧ ( 𝑏𝐴 ∧ ω ⊆ 𝑏 ) ) → ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 )
38 37 expr ( ( 𝜑𝑏𝐴 ) → ( ω ⊆ 𝑏 → ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) )
39 38 ralrimiva ( 𝜑 → ∀ 𝑏𝐴 ( ω ⊆ 𝑏 → ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) )
40 nfmpt1 𝑏 ( 𝑏𝐴𝐺 )
41 40 nfeq2 𝑏 𝑔 = ( 𝑏𝐴𝐺 )
42 fveq1 ( 𝑔 = ( 𝑏𝐴𝐺 ) → ( 𝑔𝑏 ) = ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) )
43 42 f1oeq1d ( 𝑔 = ( 𝑏𝐴𝐺 ) → ( ( 𝑔𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ↔ ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) )
44 43 imbi2d ( 𝑔 = ( 𝑏𝐴𝐺 ) → ( ( ω ⊆ 𝑏 → ( 𝑔𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) ↔ ( ω ⊆ 𝑏 → ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) ) )
45 41 44 ralbid ( 𝑔 = ( 𝑏𝐴𝐺 ) → ( ∀ 𝑏𝐴 ( ω ⊆ 𝑏 → ( 𝑔𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) ↔ ∀ 𝑏𝐴 ( ω ⊆ 𝑏 → ( ( 𝑏𝐴𝐺 ) ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) ) )
46 15 39 45 spcedv ( 𝜑 → ∃ 𝑔𝑏𝐴 ( ω ⊆ 𝑏 → ( 𝑔𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto𝑏 ) )