Metamath Proof Explorer

Theorem infxpenc2lem3

Description: Lemma for infxpenc2 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 7-Jul-2019)

Ref Expression
Hypotheses infxpenc2.1 ⊢ φ → A ∈ On
infxpenc2.2 ⊢ φ → ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 n ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
infxpenc2.3 ⊢ W = x ∈ On ∖ 1 𝑜 ⟼ ω ↑ 𝑜 x -1 ⁡ ran ⁡ n ⁡ b
infxpenc2.4 ⊢ φ → F : ω ↑ 𝑜 2 𝑜 ⟶ 1-1 onto ω
infxpenc2.5 ⊢ φ → F ⁡ ∅ = ∅
Assertion infxpenc2lem3 ⊢ φ → ∃ g ∀ b ∈ A ω ⊆ b → g ⁡ b : b × b ⟶ 1-1 onto b

Proof

Step Hyp Ref Expression
1 infxpenc2.1 ⊢ φ → A ∈ On
2 infxpenc2.2 ⊢ φ → ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 n ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
3 infxpenc2.3 ⊢ W = x ∈ On ∖ 1 𝑜 ⟼ ω ↑ 𝑜 x -1 ⁡ ran ⁡ n ⁡ b
4 infxpenc2.4 ⊢ φ → F : ω ↑ 𝑜 2 𝑜 ⟶ 1-1 onto ω
5 infxpenc2.5 ⊢ φ → F ⁡ ∅ = ∅
6 eqid ⊢ y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1 = y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1
7 eqid ⊢ ω CNF W ∘ y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1 ∘ ω ↑ 𝑜 2 𝑜 CNF W -1 = ω CNF W ∘ y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1 ∘ ω ↑ 𝑜 2 𝑜 CNF W -1
8 eqid ⊢ y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z ∘ z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w -1 -1 = y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z ∘ z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w -1 -1
9 eqid ⊢ z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w = z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w
10 eqid ⊢ z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z = z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z
11 eqid ⊢ ω CNF 2 𝑜 ⋅ 𝑜 W ∘ y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z ∘ z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w -1 -1 ∘ ω CNF W ⋅ 𝑜 2 𝑜 -1 = ω CNF 2 𝑜 ⋅ 𝑜 W ∘ y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z ∘ z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w -1 -1 ∘ ω CNF W ⋅ 𝑜 2 𝑜 -1
12 eqid ⊢ x ∈ ω ↑ 𝑜 W , y ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 x + 𝑜 y = x ∈ ω ↑ 𝑜 W , y ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 x + 𝑜 y
13 eqid ⊢ x ∈ b , y ∈ b ⟼ n ⁡ b ⁡ x n ⁡ b ⁡ y = x ∈ b , y ∈ b ⟼ n ⁡ b ⁡ x n ⁡ b ⁡ y
14 eqid ⊢ n ⁡ b -1 ∘ ω CNF W ∘ y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1 ∘ ω ↑ 𝑜 2 𝑜 CNF W -1 ∘ ω CNF 2 𝑜 ⋅ 𝑜 W ∘ y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z ∘ z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w -1 -1 ∘ ω CNF W ⋅ 𝑜 2 𝑜 -1 ∘ x ∈ ω ↑ 𝑜 W , y ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 x + 𝑜 y ∘ x ∈ b , y ∈ b ⟼ n ⁡ b ⁡ x n ⁡ b ⁡ y = n ⁡ b -1 ∘ ω CNF W ∘ y ∈ x ∈ ω ↑ 𝑜 2 𝑜 W | finSupp ∅⁡ x ⟼ F ∘ y ∘ I ↾ W -1 ∘ ω ↑ 𝑜 2 𝑜 CNF W -1 ∘ ω CNF 2 𝑜 ⋅ 𝑜 W ∘ y ∈ x ∈ ω W ⋅ 𝑜 2 𝑜 | finSupp ∅⁡ x ⟼ I ↾ ω ∘ y ∘ z ∈ 2 𝑜 , w ∈ W ⟼ 2 𝑜 ⋅ 𝑜 w + 𝑜 z ∘ z ∈ 2 𝑜 , w ∈ W ⟼ W ⋅ 𝑜 z + 𝑜 w -1 -1 ∘ ω CNF W ⋅ 𝑜 2 𝑜 -1 ∘ x ∈ ω ↑ 𝑜 W , y ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 x + 𝑜 y ∘ x ∈ b , y ∈ b ⟼ n ⁡ b ⁡ x n ⁡ b ⁡ y
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 infxpenc2lem2 ⊢ φ → ∃ g ∀ b ∈ A ω ⊆ b → g ⁡ b : b × b ⟶ 1-1 onto b