Metamath Proof Explorer

Theorem cantnfval

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 cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
cantnfcl.g ⊢ G = OrdIso E F supp ∅
cantnfcl.f ⊢ φ → F ∈ S
cantnfval.h ⊢ H = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z ∅
Assertion cantnfval ⊢ φ → A CNF B ⁡ F = H ⁡ dom ⁡ G

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 cantnfcl.g ⊢ G = OrdIso E F supp ∅
5 cantnfcl.f ⊢ φ → F ∈ S
6 cantnfval.h ⊢ H = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z ∅
7 eqid ⊢ g ∈ A B | finSupp ∅⁡ g = g ∈ A B | finSupp ∅⁡ g
8 7 2 3 cantnffval ⊢ φ → A CNF B = f ∈ g ∈ A B | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
9 8 fveq1d ⊢ φ → A CNF B ⁡ F = f ∈ g ∈ A B | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ⁡ F
10 7 2 3 cantnfdm ⊢ φ → dom ⁡ A CNF B = g ∈ A B | finSupp ∅⁡ g
11 1 10 eqtrid ⊢ φ → S = g ∈ A B | finSupp ∅⁡ g
12 5 11 eleqtrd ⊢ φ → F ∈ g ∈ A B | finSupp ∅⁡ g
13 ovex ⊢ f supp ∅ ∈ V
14 eqid ⊢ OrdIso E f supp ∅ = OrdIso E f supp ∅
15 14 oiexg ⊢ f supp ∅ ∈ V → OrdIso E f supp ∅ ∈ V
16 13 15 mp1i ⊢ f = F → OrdIso E f supp ∅ ∈ V
17 simpr ⊢ f = F ∧ h = OrdIso E f supp ∅ → h = OrdIso E f supp ∅
18 oveq1 ⊢ f = F → f supp ∅ = F supp ∅
19 18 adantr ⊢ f = F ∧ h = OrdIso E f supp ∅ → f supp ∅ = F supp ∅
20 oieq2 ⊢ f supp ∅ = F supp ∅ → OrdIso E f supp ∅ = OrdIso E F supp ∅
21 19 20 syl ⊢ f = F ∧ h = OrdIso E f supp ∅ → OrdIso E f supp ∅ = OrdIso E F supp ∅
22 17 21 eqtrd ⊢ f = F ∧ h = OrdIso E f supp ∅ → h = OrdIso E F supp ∅
23 22 4 eqtr4di ⊢ f = F ∧ h = OrdIso E f supp ∅ → h = G
24 23 fveq1d ⊢ f = F ∧ h = OrdIso E f supp ∅ → h ⁡ k = G ⁡ k
25 24 oveq2d ⊢ f = F ∧ h = OrdIso E f supp ∅ → A ↑ 𝑜 h ⁡ k = A ↑ 𝑜 G ⁡ k
26 simpl ⊢ f = F ∧ h = OrdIso E f supp ∅ → f = F
27 26 24 fveq12d ⊢ f = F ∧ h = OrdIso E f supp ∅ → f ⁡ h ⁡ k = F ⁡ G ⁡ k
28 25 27 oveq12d ⊢ f = F ∧ h = OrdIso E f supp ∅ → A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k = A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k
29 28 oveq1d ⊢ f = F ∧ h = OrdIso E f supp ∅ → A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z = A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z
30 29 mpoeq3dv ⊢ f = F ∧ h = OrdIso E f supp ∅ → k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z = k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z
31 eqid ⊢ ∅ = ∅
32 seqomeq12 ⊢ k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z = k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z ∧ ∅ = ∅ → seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z ∅
33 30 31 32 sylancl ⊢ f = F ∧ h = OrdIso E f supp ∅ → seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k + 𝑜 z ∅
34 33 6 eqtr4di ⊢ f = F ∧ h = OrdIso E f supp ∅ → seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ = H
35 23 dmeqd ⊢ f = F ∧ h = OrdIso E f supp ∅ → dom ⁡ h = dom ⁡ G
36 34 35 fveq12d ⊢ f = F ∧ h = OrdIso E f supp ∅ → seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = H ⁡ dom ⁡ G
37 16 36 csbied ⊢ f = F → ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = H ⁡ dom ⁡ G
38 eqid ⊢ f ∈ g ∈ A B | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h = f ∈ g ∈ A B | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h
39 fvex ⊢ H ⁡ dom ⁡ G ∈ V
40 37 38 39 fvmpt ⊢ F ∈ g ∈ A B | finSupp ∅⁡ g → f ∈ g ∈ A B | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ⁡ F = H ⁡ dom ⁡ G
41 12 40 syl ⊢ φ → f ∈ g ∈ A B | finSupp ∅⁡ g ⟼ ⦋ OrdIso E f supp ∅ / h⦌ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 h ⁡ k ⋅ 𝑜 f ⁡ h ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ h ⁡ F = H ⁡ dom ⁡ G
42 9 41 eqtrd ⊢ φ → A CNF B ⁡ F = H ⁡ dom ⁡ G