Theorem infxpenc2

Description: Existence form of infxpenc . A "uniform" or "canonical" version of infxpen , asserting the existence of a single function g that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Assertion	infxpenc2	⊢ ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		cnfcom3c	⊢ ( 𝐴 ∈ On → ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) )
2		df-2o	⊢ 2o = suc 1o
3	2	oveq2i	⊢ ( ω ↑o 2o ) = ( ω ↑o suc 1o )
4		omelon	⊢ ω ∈ On
5		1on	⊢ 1o ∈ On
6		oesuc	⊢ ( ( ω ∈ On ∧ 1o ∈ On ) → ( ω ↑o suc 1o ) = ( ( ω ↑o 1o ) ·o ω ) )
7	4 5 6	mp2an	⊢ ( ω ↑o suc 1o ) = ( ( ω ↑o 1o ) ·o ω )
8		oe1	⊢ ( ω ∈ On → ( ω ↑o 1o ) = ω )
9	4 8	ax-mp	⊢ ( ω ↑o 1o ) = ω
10	9	oveq1i	⊢ ( ( ω ↑o 1o ) ·o ω ) = ( ω ·o ω )
11	3 7 10	3eqtri	⊢ ( ω ↑o 2o ) = ( ω ·o ω )
12		omxpen	⊢ ( ( ω ∈ On ∧ ω ∈ On ) → ( ω ·o ω ) ≈ ( ω × ω ) )
13	4 4 12	mp2an	⊢ ( ω ·o ω ) ≈ ( ω × ω )
14	11 13	eqbrtri	⊢ ( ω ↑o 2o ) ≈ ( ω × ω )
15		xpomen	⊢ ( ω × ω ) ≈ ω
16	14 15	entri	⊢ ( ω ↑o 2o ) ≈ ω
17	16	a1i	⊢ ( 𝐴 ∈ On → ( ω ↑o 2o ) ≈ ω )
18		bren	⊢ ( ( ω ↑o 2o ) ≈ ω ↔ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω )
19	17 18	sylib	⊢ ( 𝐴 ∈ On → ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω )
20		exdistrv	⊢ ( ∃ 𝑛 ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ↔ ( ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) )
21		simpl	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → 𝐴 ∈ On )
22		simprl	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) )
23		sseq2	⊢ ( 𝑥 = 𝑏 → ( ω ⊆ 𝑥 ↔ ω ⊆ 𝑏 ) )
24		oveq2	⊢ ( 𝑦 = 𝑤 → ( ω ↑o 𝑦 ) = ( ω ↑o 𝑤 ) )
25	24	f1oeq3d	⊢ ( 𝑦 = 𝑤 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ↔ ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
26	25	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) )
27		fveq2	⊢ ( 𝑥 = 𝑏 → ( 𝑛 ‘ 𝑥 ) = ( 𝑛 ‘ 𝑏 ) )
28		f1oeq1	⊢ ( ( 𝑛 ‘ 𝑥 ) = ( 𝑛 ‘ 𝑏 ) → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
29	27 28	syl	⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
30		f1oeq2	⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑏 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
31	29 30	bitrd	⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
32	31	rexbidv	⊢ ( 𝑥 = 𝑏 → ( ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
33	26 32	syl5bb	⊢ ( 𝑥 = 𝑏 → ( ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
34	23 33	imbi12d	⊢ ( 𝑥 = 𝑏 → ( ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ↔ ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) )
35	34	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ↔ ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
36	22 35	sylib	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
37		oveq2	⊢ ( 𝑏 = 𝑧 → ( ω ↑o 𝑏 ) = ( ω ↑o 𝑧 ) )
38	37	cbvmptv	⊢ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) = ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) )
39	38	cnveqi	⊢ ◡ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) = ◡ ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) )
40	39	fveq1i	⊢ ( ◡ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) ) = ( ◡ ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) )
41		2on	⊢ 2o ∈ On
42		peano1	⊢ ∅ ∈ ω
43		oen0	⊢ ( ( ( ω ∈ On ∧ 2o ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 2o ) )
44	42 43	mpan2	⊢ ( ( ω ∈ On ∧ 2o ∈ On ) → ∅ ∈ ( ω ↑o 2o ) )
45	4 41 44	mp2an	⊢ ∅ ∈ ( ω ↑o 2o )
46		eqid	⊢ ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) = ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) )
47	46	fveqf1o	⊢ ( ( 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ∅ ∈ ( ω ↑o 2o ) ∧ ∅ ∈ ω ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ ) )
48	45 42 47	mp3an23	⊢ ( 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ ) )
49	48	ad2antll	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ ) )
50	49	simpld	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω )
51	49	simprd	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ )
52	21 36 40 50 51	infxpenc2lem3	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
53	52	ex	⊢ ( 𝐴 ∈ On → ( ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
54	53	exlimdvv	⊢ ( 𝐴 ∈ On → ( ∃ 𝑛 ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
55	20 54	syl5bir	⊢ ( 𝐴 ∈ On → ( ( ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
56	1 19 55	mp2and	⊢ ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )