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	27	f1oeq1d	⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
29		f1oeq2	⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑏 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
30	28 29	bitrd	⊢ ( 𝑥 = 𝑏 → ( ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
31	30	rexbidv	⊢ ( 𝑥 = 𝑏 → ( ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
32	26 31	syl5bb	⊢ ( 𝑥 = 𝑏 → ( ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
33	23 32	imbi12d	⊢ ( 𝑥 = 𝑏 → ( ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ↔ ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) )
34	33	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ↔ ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
35	22 34	sylib	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
36		oveq2	⊢ ( 𝑏 = 𝑧 → ( ω ↑o 𝑏 ) = ( ω ↑o 𝑧 ) )
37	36	cbvmptv	⊢ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) = ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) )
38	37	cnveqi	⊢ ◡ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) = ◡ ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) )
39	38	fveq1i	⊢ ( ◡ ( 𝑏 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑏 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) ) = ( ◡ ( 𝑧 ∈ ( On ∖ 1o ) ↦ ( ω ↑o 𝑧 ) ) ‘ ran ( 𝑛 ‘ 𝑏 ) )
40		2on	⊢ 2o ∈ On
41		peano1	⊢ ∅ ∈ ω
42		oen0	⊢ ( ( ( ω ∈ On ∧ 2o ∈ On ) ∧ ∅ ∈ ω ) → ∅ ∈ ( ω ↑o 2o ) )
43	41 42	mpan2	⊢ ( ( ω ∈ On ∧ 2o ∈ On ) → ∅ ∈ ( ω ↑o 2o ) )
44	4 40 43	mp2an	⊢ ∅ ∈ ( ω ↑o 2o )
45		eqid	⊢ ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) = ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) )
46	45	fveqf1o	⊢ ( ( 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ∅ ∈ ( ω ↑o 2o ) ∧ ∅ ∈ ω ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ ) )
47	44 41 46	mp3an23	⊢ ( 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ ) )
48	47	ad2antll	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω ∧ ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ ) )
49	48	simpld	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) : ( ω ↑o 2o ) –1-1-onto→ ω )
50	48	simprd	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ( ( 𝑓 ∘ ( ( I ↾ ( ( ω ↑o 2o ) ∖ { ∅ , ( ◡ 𝑓 ‘ ∅ ) } ) ) ∪ { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ , ⟨ ( ◡ 𝑓 ‘ ∅ ) , ∅ ⟩ } ) ) ‘ ∅ ) = ∅ )
51	21 35 39 49 50	infxpenc2lem3	⊢ ( ( 𝐴 ∈ On ∧ ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )
52	51	ex	⊢ ( 𝐴 ∈ On → ( ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
53	52	exlimdvv	⊢ ( 𝐴 ∈ On → ( ∃ 𝑛 ∃ 𝑓 ( ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
54	20 53	syl5bir	⊢ ( 𝐴 ∈ On → ( ( ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
55	1 19 54	mp2and	⊢ ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )