Metamath Proof Explorer


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