Metamath Proof Explorer

Theorem cantnflem1d

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
oemapval.f ⊢ φ → F ∈ S
oemapval.g ⊢ φ → G ∈ S
oemapvali.r ⊢ φ → F T G
oemapvali.x ⊢ X = ⋃ c ∈ B | F ⁡ c ∈ G ⁡ c
cantnflem1.o ⊢ O = OrdIso E G supp ∅
cantnflem1.h ⊢ H = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 O ⁡ k ⋅ 𝑜 G ⁡ O ⁡ k + 𝑜 z ∅
Assertion cantnflem1d ⊢ φ → A CNF B ⁡ x ∈ B ⟼ if x ⊆ X F ⁡ x ∅ ∈ H ⁡ suc ⁡ O -1 ⁡ 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 oemapval.t ⊢ T = x y | ∃ z ∈ B x ⁡ z ∈ y ⁡ z ∧ ∀ w ∈ B z ∈ w → x ⁡ w = y ⁡ w
5 oemapval.f ⊢ φ → F ∈ S
6 oemapval.g ⊢ φ → G ∈ S
7 oemapvali.r ⊢ φ → F T G
8 oemapvali.x ⊢ X = ⋃ c ∈ B | F ⁡ c ∈ G ⁡ c
9 cantnflem1.o ⊢ O = OrdIso E G supp ∅
10 cantnflem1.h ⊢ H = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 O ⁡ k ⋅ 𝑜 G ⁡ O ⁡ k + 𝑜 z ∅
11 1 2 3 4 5 6 7 8 oemapvali ⊢ φ → X ∈ B ∧ F ⁡ X ∈ G ⁡ X ∧ ∀ w ∈ B X ∈ w → F ⁡ w = G ⁡ w
12 11 simp1d ⊢ φ → X ∈ B
13 onelon ⊢ B ∈ On ∧ X ∈ B → X ∈ On
14 3 12 13 syl2anc ⊢ φ → X ∈ On
15 oecl ⊢ A ∈ On ∧ X ∈ On → A ↑ 𝑜 X ∈ On
16 2 14 15 syl2anc ⊢ φ → A ↑ 𝑜 X ∈ On
17 1 2 3 cantnfs ⊢ φ → G ∈ S ↔ G : B ⟶ A ∧ finSupp ∅⁡ G
18 6 17 mpbid ⊢ φ → G : B ⟶ A ∧ finSupp ∅⁡ G
19 18 simpld ⊢ φ → G : B ⟶ A
20 19 12 ffvelrnd ⊢ φ → G ⁡ X ∈ A
21 onelon ⊢ A ∈ On ∧ G ⁡ X ∈ A → G ⁡ X ∈ On
22 2 20 21 syl2anc ⊢ φ → G ⁡ X ∈ On
23 omcl ⊢ A ↑ 𝑜 X ∈ On ∧ G ⁡ X ∈ On → A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X ∈ On
24 16 22 23 syl2anc ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X ∈ On
25 ovexd ⊢ φ → G supp ∅ ∈ V
26 1 2 3 9 6 cantnfcl ⊢ φ → E We supp ∅⁡ G ∧ dom ⁡ O ∈ ω
27 26 simpld ⊢ φ → E We supp ∅⁡ G
28 9 oiiso ⊢ G supp ∅ ∈ V ∧ E We supp ∅⁡ G → O Isom E , E dom ⁡ O G supp ∅
29 25 27 28 syl2anc ⊢ φ → O Isom E , E dom ⁡ O G supp ∅
30 isof1o ⊢ O Isom E , E dom ⁡ O G supp ∅ → O : dom ⁡ O ⟶ 1-1 onto G supp ∅
31 29 30 syl ⊢ φ → O : dom ⁡ O ⟶ 1-1 onto G supp ∅
32 f1ocnv ⊢ O : dom ⁡ O ⟶ 1-1 onto G supp ∅ → O -1 : G supp ∅ ⟶ 1-1 onto dom ⁡ O
33 f1of ⊢ O -1 : G supp ∅ ⟶ 1-1 onto dom ⁡ O → O -1 : G supp ∅ ⟶ dom ⁡ O
34 31 32 33 3syl ⊢ φ → O -1 : G supp ∅ ⟶ dom ⁡ O
35 1 2 3 4 5 6 7 8 cantnflem1a ⊢ φ → X ∈ supp ∅⁡ G
36 34 35 ffvelrnd ⊢ φ → O -1 ⁡ X ∈ dom ⁡ O
37 26 simprd ⊢ φ → dom ⁡ O ∈ ω
38 elnn ⊢ O -1 ⁡ X ∈ dom ⁡ O ∧ dom ⁡ O ∈ ω → O -1 ⁡ X ∈ ω
39 36 37 38 syl2anc ⊢ φ → O -1 ⁡ X ∈ ω
40 10 cantnfvalf ⊢ H : ω ⟶ On
41 40 ffvelrni ⊢ O -1 ⁡ X ∈ ω → H ⁡ O -1 ⁡ X ∈ On
42 39 41 syl ⊢ φ → H ⁡ O -1 ⁡ X ∈ On
43 oaword1 ⊢ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X ∈ On ∧ H ⁡ O -1 ⁡ X ∈ On → A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X ⊆ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X + 𝑜 H ⁡ O -1 ⁡ X
44 24 42 43 syl2anc ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X ⊆ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X + 𝑜 H ⁡ O -1 ⁡ X
45 1 2 3 9 6 10 cantnfsuc ⊢ φ ∧ O -1 ⁡ X ∈ ω → H ⁡ suc ⁡ O -1 ⁡ X = A ↑ 𝑜 O ⁡ O -1 ⁡ X ⋅ 𝑜 G ⁡ O ⁡ O -1 ⁡ X + 𝑜 H ⁡ O -1 ⁡ X
46 39 45 mpdan ⊢ φ → H ⁡ suc ⁡ O -1 ⁡ X = A ↑ 𝑜 O ⁡ O -1 ⁡ X ⋅ 𝑜 G ⁡ O ⁡ O -1 ⁡ X + 𝑜 H ⁡ O -1 ⁡ X
47 f1ocnvfv2 ⊢ O : dom ⁡ O ⟶ 1-1 onto G supp ∅ ∧ X ∈ supp ∅⁡ G → O ⁡ O -1 ⁡ X = X
48 31 35 47 syl2anc ⊢ φ → O ⁡ O -1 ⁡ X = X
49 48 oveq2d ⊢ φ → A ↑ 𝑜 O ⁡ O -1 ⁡ X = A ↑ 𝑜 X
50 48 fveq2d ⊢ φ → G ⁡ O ⁡ O -1 ⁡ X = G ⁡ X
51 49 50 oveq12d ⊢ φ → A ↑ 𝑜 O ⁡ O -1 ⁡ X ⋅ 𝑜 G ⁡ O ⁡ O -1 ⁡ X = A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X
52 51 oveq1d ⊢ φ → A ↑ 𝑜 O ⁡ O -1 ⁡ X ⋅ 𝑜 G ⁡ O ⁡ O -1 ⁡ X + 𝑜 H ⁡ O -1 ⁡ X = A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X + 𝑜 H ⁡ O -1 ⁡ X
53 46 52 eqtrd ⊢ φ → H ⁡ suc ⁡ O -1 ⁡ X = A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X + 𝑜 H ⁡ O -1 ⁡ X
54 44 53 sseqtrrd ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X ⊆ H ⁡ suc ⁡ O -1 ⁡ X
55 onss ⊢ B ∈ On → B ⊆ On
56 3 55 syl ⊢ φ → B ⊆ On
57 56 sselda ⊢ φ ∧ x ∈ B → x ∈ On
58 14 adantr ⊢ φ ∧ x ∈ B → X ∈ On
59 onsseleq ⊢ x ∈ On ∧ X ∈ On → x ⊆ X ↔ x ∈ X ∨ x = X
60 57 58 59 syl2anc ⊢ φ ∧ x ∈ B → x ⊆ X ↔ x ∈ X ∨ x = X
61 orcom ⊢ x ∈ X ∨ x = X ↔ x = X ∨ x ∈ X
62 60 61 bitrdi ⊢ φ ∧ x ∈ B → x ⊆ X ↔ x = X ∨ x ∈ X
63 62 ifbid ⊢ φ ∧ x ∈ B → if x ⊆ X F ⁡ x ∅ = if x = X ∨ x ∈ X F ⁡ x ∅
64 63 mpteq2dva ⊢ φ → x ∈ B ⟼ if x ⊆ X F ⁡ x ∅ = x ∈ B ⟼ if x = X ∨ x ∈ X F ⁡ x ∅
65 64 fveq2d ⊢ φ → A CNF B ⁡ x ∈ B ⟼ if x ⊆ X F ⁡ x ∅ = A CNF B ⁡ x ∈ B ⟼ if x = X ∨ x ∈ X F ⁡ x ∅
66 1 2 3 cantnfs ⊢ φ → F ∈ S ↔ F : B ⟶ A ∧ finSupp ∅⁡ F
67 5 66 mpbid ⊢ φ → F : B ⟶ A ∧ finSupp ∅⁡ F
68 67 simpld ⊢ φ → F : B ⟶ A
69 68 ffvelrnda ⊢ φ ∧ y ∈ B → F ⁡ y ∈ A
70 20 ne0d ⊢ φ → A ≠ ∅
71 on0eln0 ⊢ A ∈ On → ∅ ∈ A ↔ A ≠ ∅
72 2 71 syl ⊢ φ → ∅ ∈ A ↔ A ≠ ∅
73 70 72 mpbird ⊢ φ → ∅ ∈ A
74 73 adantr ⊢ φ ∧ y ∈ B → ∅ ∈ A
75 69 74 ifcld ⊢ φ ∧ y ∈ B → if y ∈ X F ⁡ y ∅ ∈ A
76 75 fmpttd ⊢ φ → y ∈ B ⟼ if y ∈ X F ⁡ y ∅ : B ⟶ A
77 0ex ⊢ ∅ ∈ V
78 77 a1i ⊢ φ → ∅ ∈ V
79 67 simprd ⊢ φ → finSupp ∅⁡ F
80 68 3 78 79 fsuppmptif ⊢ φ → finSupp ∅⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅
81 1 2 3 cantnfs ⊢ φ → y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ S ↔ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ : B ⟶ A ∧ finSupp ∅⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅
82 76 80 81 mpbir2and ⊢ φ → y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ S
83 68 12 ffvelrnd ⊢ φ → F ⁡ X ∈ A
84 eldifn ⊢ y ∈ B ∖ X → ¬ y ∈ X
85 84 adantl ⊢ φ ∧ y ∈ B ∖ X → ¬ y ∈ X
86 85 iffalsed ⊢ φ ∧ y ∈ B ∖ X → if y ∈ X F ⁡ y ∅ = ∅
87 86 3 suppss2 ⊢ φ → y ∈ B ⟼ if y ∈ X F ⁡ y ∅ supp ∅ ⊆ X
88 ifor ⊢ if x = X ∨ x ∈ X F ⁡ x ∅ = if x = X F ⁡ x if x ∈ X F ⁡ x ∅
89 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
90 89 adantl ⊢ x ∈ B ∧ x = X → F ⁡ x = F ⁡ X
91 90 ifeq1da ⊢ x ∈ B → if x = X F ⁡ x y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ⁡ x = if x = X F ⁡ X y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ⁡ x
92 eleq1w ⊢ y = x → y ∈ X ↔ x ∈ X
93 fveq2 ⊢ y = x → F ⁡ y = F ⁡ x
94 92 93 ifbieq1d ⊢ y = x → if y ∈ X F ⁡ y ∅ = if x ∈ X F ⁡ x ∅
95 eqid ⊢ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ = y ∈ B ⟼ if y ∈ X F ⁡ y ∅
96 fvex ⊢ F ⁡ x ∈ V
97 96 77 ifex ⊢ if x ∈ X F ⁡ x ∅ ∈ V
98 94 95 97 fvmpt ⊢ x ∈ B → y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ⁡ x = if x ∈ X F ⁡ x ∅
99 98 ifeq2d ⊢ x ∈ B → if x = X F ⁡ x y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ⁡ x = if x = X F ⁡ x if x ∈ X F ⁡ x ∅
100 91 99 eqtr3d ⊢ x ∈ B → if x = X F ⁡ X y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ⁡ x = if x = X F ⁡ x if x ∈ X F ⁡ x ∅
101 88 100 eqtr4id ⊢ x ∈ B → if x = X ∨ x ∈ X F ⁡ x ∅ = if x = X F ⁡ X y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ⁡ x
102 101 mpteq2ia ⊢ x ∈ B ⟼ if x = X ∨ x ∈ X F ⁡ x ∅ = x ∈ B ⟼ if x = X F ⁡ X y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ⁡ x
103 1 2 3 82 12 83 87 102 cantnfp1 ⊢ φ → x ∈ B ⟼ if x = X ∨ x ∈ X F ⁡ x ∅ ∈ S ∧ A CNF B ⁡ x ∈ B ⟼ if x = X ∨ x ∈ X F ⁡ x ∅ = A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅
104 103 simprd ⊢ φ → A CNF B ⁡ x ∈ B ⟼ if x = X ∨ x ∈ X F ⁡ x ∅ = A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅
105 65 104 eqtrd ⊢ φ → A CNF B ⁡ x ∈ B ⟼ if x ⊆ X F ⁡ x ∅ = A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅
106 onelon ⊢ A ∈ On ∧ F ⁡ X ∈ A → F ⁡ X ∈ On
107 2 83 106 syl2anc ⊢ φ → F ⁡ X ∈ On
108 omsuc ⊢ A ↑ 𝑜 X ∈ On ∧ F ⁡ X ∈ On → A ↑ 𝑜 X ⋅ 𝑜 suc ⁡ F ⁡ X = A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A ↑ 𝑜 X
109 16 107 108 syl2anc ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 suc ⁡ F ⁡ X = A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A ↑ 𝑜 X
110 eloni ⊢ G ⁡ X ∈ On → Ord ⁡ G ⁡ X
111 22 110 syl ⊢ φ → Ord ⁡ G ⁡ X
112 11 simp2d ⊢ φ → F ⁡ X ∈ G ⁡ X
113 ordsucss ⊢ Ord ⁡ G ⁡ X → F ⁡ X ∈ G ⁡ X → suc ⁡ F ⁡ X ⊆ G ⁡ X
114 111 112 113 sylc ⊢ φ → suc ⁡ F ⁡ X ⊆ G ⁡ X
115 suceloni ⊢ F ⁡ X ∈ On → suc ⁡ F ⁡ X ∈ On
116 107 115 syl ⊢ φ → suc ⁡ F ⁡ X ∈ On
117 omwordi ⊢ suc ⁡ F ⁡ X ∈ On ∧ G ⁡ X ∈ On ∧ A ↑ 𝑜 X ∈ On → suc ⁡ F ⁡ X ⊆ G ⁡ X → A ↑ 𝑜 X ⋅ 𝑜 suc ⁡ F ⁡ X ⊆ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X
118 116 22 16 117 syl3anc ⊢ φ → suc ⁡ F ⁡ X ⊆ G ⁡ X → A ↑ 𝑜 X ⋅ 𝑜 suc ⁡ F ⁡ X ⊆ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X
119 114 118 mpd ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 suc ⁡ F ⁡ X ⊆ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X
120 109 119 eqsstrrd ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A ↑ 𝑜 X ⊆ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X
121 1 2 3 82 73 14 87 cantnflt2 ⊢ φ → A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X
122 onelon ⊢ A ↑ 𝑜 X ∈ On ∧ A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X → A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ On
123 16 121 122 syl2anc ⊢ φ → A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ On
124 omcl ⊢ A ↑ 𝑜 X ∈ On ∧ F ⁡ X ∈ On → A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X ∈ On
125 16 107 124 syl2anc ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X ∈ On
126 oaord ⊢ A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ On ∧ A ↑ 𝑜 X ∈ On ∧ A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X ∈ On → A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X ↔ A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A ↑ 𝑜 X
127 123 16 125 126 syl3anc ⊢ φ → A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X ↔ A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A ↑ 𝑜 X
128 121 127 mpbid ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A ↑ 𝑜 X
129 120 128 sseldd ⊢ φ → A ↑ 𝑜 X ⋅ 𝑜 F ⁡ X + 𝑜 A CNF B ⁡ y ∈ B ⟼ if y ∈ X F ⁡ y ∅ ∈ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X
130 105 129 eqeltrd ⊢ φ → A CNF B ⁡ x ∈ B ⟼ if x ⊆ X F ⁡ x ∅ ∈ A ↑ 𝑜 X ⋅ 𝑜 G ⁡ X
131 54 130 sseldd ⊢ φ → A CNF B ⁡ x ∈ B ⟼ if x ⊆ X F ⁡ x ∅ ∈ H ⁡ suc ⁡ O -1 ⁡ X