This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( 𝑥 = 𝑏 → ( ∃ 𝑦 ∈ ( 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 biimtrrid ⊢ ( 𝐴 ∈ On → ( ( ∃ 𝑛 ∀ 𝑥 ∈ 𝐴 ( ω ⊆ 𝑥 → ∃ 𝑦 ∈ ( On ∖ 1o ) ( 𝑛 ‘ 𝑥 ) : 𝑥 –1-1-onto→ ( ω ↑o 𝑦 ) ) ∧ ∃ 𝑓 𝑓 : ( ω ↑o 2o ) –1-1-onto→ ω ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) ) )
55 1 19 54 mp2and ⊢ ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ( 𝑔 ‘ 𝑏 ) : ( 𝑏 × 𝑏 ) –1-1-onto→ 𝑏 ) )