Metamath Proof Explorer

Theorem cantnffval

Description: The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnffval.s ⊢ S = g ∈ A B | finSupp ∅⁡ g
cantnffval.a ⊢ φ → A ∈ On
cantnffval.b ⊢ φ → B ∈ On
Assertion cantnffval ⊢ φ → A CNF B = f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h

Proof

Step Hyp Ref Expression
1 cantnffval.s ⊢ S = g ∈ A B | finSupp ∅⁡ g
2 cantnffval.a ⊢ φ → A ∈ On
3 cantnffval.b ⊢ φ → B ∈ On
4 oveq12 ⊢ x = A ∧ y = B → x y = A B
5 4 rabeqdv ⊢ x = A ∧ y = B → g ∈ x y | finSupp ∅⁡ g = g ∈ A B | finSupp ∅⁡ g
6 5 1 eqtr4di ⊢ x = A ∧ y = B → g ∈ x y | finSupp ∅⁡ g = S
7 simp1l ⊢ x = A ∧ y = B ∧ k ∈ V ∧ z ∈ V → x = A
8 7 oveq1d ⊢ x = A ∧ y = B ∧ k ∈ V ∧ z ∈ V → x ↑ 𝑜 h ⁡ k = A ↑ 𝑜 h ⁡ k
9 8 oveq1d ⊢ x = A ∧ y = B ∧ k ∈ V ∧ z ∈ V → x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k = A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k
10 9 oveq1d ⊢ x = A ∧ y = B ∧ k ∈ V ∧ z ∈ V → x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z = A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z
11 10 mpoeq3dva ⊢ x = A ∧ y = B → k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z = k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z
12 eqid ⊢ ∅ = ∅
13 seqomeq12 ⊢ k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z = k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∧ ∅ = ∅ → seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅
14 11 12 13 sylancl ⊢ x = A ∧ y = B → seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅
15 14 fveq1d ⊢ x = A ∧ y = B → seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
16 15 csbeq2dv ⊢ x = A ∧ y = B → ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
17 6 16 mpteq12dv ⊢ x = A ∧ y = B → f ∈ g ∈ x y | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
18 df-cnf ⊢ CNF = x ∈ On , y ∈ On ⟼ f ∈ g ∈ x y | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ x ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
19 ovex ⊢ A B ∈ V
20 1 19 rabex2 ⊢ S ∈ V
21 20 mptex ⊢ f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ∈ V
22 17 18 21 ovmpoa ⊢ A ∈ On ∧ B ∈ On → A CNF B = f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
23 2 3 22 syl2anc ⊢ φ → A CNF B = f ∈ S ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h