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→ 𝑏 ) )