This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem infxpenc2lem3

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 ⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) = ∅ )
Assertion infxpenc2lem3 ( 𝜑 → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –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 eqid ⊢ ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) )
7 eqid ⊢ ( ( ( ω CNF 𝑊 ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) ) ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) ) = ( ( ( ω CNF 𝑊 ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) ) ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) )
8 eqid ⊢ ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) ) ∘ ◡ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) ) ) ) ) ) = ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) ) ∘ ◡ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) ) ) ) ) )
9 eqid ⊢ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) ) = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) )
10 eqid ⊢ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) ) = ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) )
11 eqid ⊢ ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) ) ∘ ◡ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) ) ) ) ) ) ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) ) = ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) ) ∘ ◡ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) ) ) ) ) ) ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) )
12 eqid ⊢ ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) ) = ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) )
13 eqid ⊢ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ⟨ ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑥 ) , ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑦 ) ⟩ ) = ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ⟨ ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑥 ) , ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑦 ) ⟩ )
14 eqid ⊢ ( ◡ ( 𝑛 ‘ 𝑏 ) ∘ ( ( ( ( ( ( ω CNF 𝑊 ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) ) ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) ) ∘ ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) ) ∘ ◡ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) ) ) ) ) ) ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) ) ) ∘ ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) ) ) ∘ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ⟨ ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑥 ) , ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑦 ) ⟩ ) ) ) = ( ◡ ( 𝑛 ‘ 𝑏 ) ∘ ( ( ( ( ( ( ω CNF 𝑊 ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ( ω ↑o 2o ) ↑m 𝑊 ) ∣ 𝑥 finSupp ∅ } ↦ ( 𝐹 ∘ ( 𝑦 ∘ ◡ ( I ↾ 𝑊 ) ) ) ) ) ∘ ◡ ( ( ω ↑o 2o ) CNF 𝑊 ) ) ∘ ( ( ( ω CNF ( 2o ·o 𝑊 ) ) ∘ ( 𝑦 ∈ { 𝑥 ∈ ( ω ↑m ( 𝑊 ·o 2o ) ) ∣ 𝑥 finSupp ∅ } ↦ ( ( I ↾ ω ) ∘ ( 𝑦 ∘ ◡ ( ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 2o ·o 𝑤 ) +o 𝑧 ) ) ∘ ◡ ( 𝑧 ∈ 2o , 𝑤 ∈ 𝑊 ↦ ( ( 𝑊 ·o 𝑧 ) +o 𝑤 ) ) ) ) ) ) ) ∘ ◡ ( ω CNF ( 𝑊 ·o 2o ) ) ) ) ∘ ( 𝑥 ∈ ( ω ↑o 𝑊 ) , 𝑦 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑥 ) +o 𝑦 ) ) ) ∘ ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ⟨ ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑥 ) , ( ( 𝑛 ‘ 𝑏 ) ‘ 𝑦 ) ⟩ ) ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 infxpenc2lem2 ⊢ ( 𝜑 → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )