Metamath Proof Explorer

Theorem cantnfres

Description: The CNF function respects extensions of the domain to a larger ordinal. (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
cantnfrescl.d ⊢ φ → D ∈ On
cantnfrescl.b ⊢ φ → B ⊆ D
cantnfrescl.x ⊢ φ ∧ n ∈ D ∖ B → X = ∅
cantnfrescl.a ⊢ φ → ∅ ∈ A
cantnfrescl.t ⊢ T = dom ⁡ A CNF D
cantnfres.m ⊢ φ → n ∈ B ⟼ X ∈ S
Assertion cantnfres ⊢ φ → A CNF B ⁡ n ∈ B ⟼ X = A CNF D ⁡ n ∈ D ⟼ X

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 cantnfrescl.d ⊢ φ → D ∈ On
5 cantnfrescl.b ⊢ φ → B ⊆ D
6 cantnfrescl.x ⊢ φ ∧ n ∈ D ∖ B → X = ∅
7 cantnfrescl.a ⊢ φ → ∅ ∈ A
8 cantnfrescl.t ⊢ T = dom ⁡ A CNF D
9 cantnfres.m ⊢ φ → n ∈ B ⟼ X ∈ S
10 4 5 6 extmptsuppeq ⊢ φ → n ∈ B ⟼ X supp ∅ = n ∈ D ⟼ X supp ∅
11 oieq2 ⊢ n ∈ B ⟼ X supp ∅ = n ∈ D ⟼ X supp ∅ → OrdIso E n ∈ B ⟼ X supp ∅ = OrdIso E n ∈ D ⟼ X supp ∅
12 10 11 syl ⊢ φ → OrdIso E n ∈ B ⟼ X supp ∅ = OrdIso E n ∈ D ⟼ X supp ∅
13 12 fveq1d ⊢ φ → OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k
14 13 3ad2ant1 ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k
15 14 oveq2d ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k
16 suppssdm ⊢ n ∈ B ⟼ X supp ∅ ⊆ dom ⁡ n ∈ B ⟼ X
17 eqid ⊢ n ∈ B ⟼ X = n ∈ B ⟼ X
18 17 dmmptss ⊢ dom ⁡ n ∈ B ⟼ X ⊆ B
19 18 a1i ⊢ φ → dom ⁡ n ∈ B ⟼ X ⊆ B
20 16 19 sstrid ⊢ φ → n ∈ B ⟼ X supp ∅ ⊆ B
21 20 3ad2ant1 ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → n ∈ B ⟼ X supp ∅ ⊆ B
22 eqid ⊢ OrdIso E n ∈ B ⟼ X supp ∅ = OrdIso E n ∈ B ⟼ X supp ∅
23 22 oif ⊢ OrdIso E n ∈ B ⟼ X supp ∅ : dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⟶ n ∈ B ⟼ X supp ∅
24 23 ffvelcdmi ⊢ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ → OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ∈ supp ∅⁡ n ∈ B ⟼ X
25 24 3ad2ant2 ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ∈ supp ∅⁡ n ∈ B ⟼ X
26 21 25 sseldd ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ∈ B
27 26 fvresd ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → n ∈ D ⟼ X ↾ B ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = n ∈ D ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k
28 5 3ad2ant1 ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → B ⊆ D
29 28 resmptd ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → n ∈ D ⟼ X ↾ B = n ∈ B ⟼ X
30 29 fveq1d ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → n ∈ D ⟼ X ↾ B ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k
31 14 fveq2d ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → n ∈ D ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k
32 27 30 31 3eqtr3d ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k
33 15 32 oveq12d ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k = A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k
34 33 oveq1d ⊢ φ ∧ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ∧ z ∈ On → A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z = A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z
35 34 mpoeq3dva ⊢ φ → k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z = k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z
36 12 dmeqd ⊢ φ → dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ = dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅
37 eqid ⊢ On = On
38 mpoeq12 ⊢ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ = dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ∧ On = On → k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z = k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z
39 36 37 38 sylancl ⊢ φ → k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z = k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z
40 35 39 eqtrd ⊢ φ → k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z = k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z
41 eqid ⊢ ∅ = ∅
42 seqomeq12 ⊢ k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z = k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z ∧ ∅ = ∅ → seq ω k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ = seq ω k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z ∅
43 40 41 42 sylancl ⊢ φ → seq ω k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ = seq ω k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z ∅
44 43 36 fveq12d ⊢ φ → seq ω k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ = seq ω k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅
45 eqid ⊢ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z ∅
46 1 2 3 22 9 45 cantnfval2 ⊢ φ → A CNF B ⁡ n ∈ B ⟼ X = seq ω k ∈ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ B ⟼ X ⁡ OrdIso E n ∈ B ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ OrdIso E n ∈ B ⟼ X supp ∅
47 eqid ⊢ OrdIso E n ∈ D ⟼ X supp ∅ = OrdIso E n ∈ D ⟼ X supp ∅
48 1 2 3 4 5 6 7 8 cantnfrescl ⊢ φ → n ∈ B ⟼ X ∈ S ↔ n ∈ D ⟼ X ∈ T
49 9 48 mpbid ⊢ φ → n ∈ D ⟼ X ∈ T
50 eqid ⊢ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z ∅
51 8 2 4 47 49 50 cantnfval2 ⊢ φ → A CNF D ⁡ n ∈ D ⟼ X = seq ω k ∈ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅ , z ∈ On ⟼ A ↑ 𝑜 OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k ⋅ 𝑜 n ∈ D ⟼ X ⁡ OrdIso E n ∈ D ⟼ X supp ∅ ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ OrdIso E n ∈ D ⟼ X supp ∅
52 44 46 51 3eqtr4d ⊢ φ → A CNF B ⁡ n ∈ B ⟼ X = A CNF D ⁡ n ∈ D ⟼ X