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