Metamath Proof Explorer

Theorem cantnfp1lem1

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 20-Jun-2015) (Revised by AV, 30-Jun-2019)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
cantnfp1.g ⊢ φ → G ∈ S
cantnfp1.x ⊢ φ → X ∈ B
cantnfp1.y ⊢ φ → Y ∈ A
cantnfp1.s ⊢ φ → G supp ∅ ⊆ X
cantnfp1.f ⊢ F = t ∈ B ⟼ if t = X Y G ⁡ t
Assertion cantnfp1lem1 ⊢ φ → F ∈ S

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 cantnfp1.g ⊢ φ → G ∈ S
5 cantnfp1.x ⊢ φ → X ∈ B
6 cantnfp1.y ⊢ φ → Y ∈ A
7 cantnfp1.s ⊢ φ → G supp ∅ ⊆ X
8 cantnfp1.f ⊢ F = t ∈ B ⟼ if t = X Y G ⁡ t
9 6 adantr ⊢ φ ∧ t ∈ B → Y ∈ A
10 1 2 3 cantnfs ⊢ φ → G ∈ S ↔ G : B ⟶ A ∧ finSupp ∅⁡ G
11 4 10 mpbid ⊢ φ → G : B ⟶ A ∧ finSupp ∅⁡ G
12 11 simpld ⊢ φ → G : B ⟶ A
13 12 ffvelrnda ⊢ φ ∧ t ∈ B → G ⁡ t ∈ A
14 9 13 ifcld ⊢ φ ∧ t ∈ B → if t = X Y G ⁡ t ∈ A
15 14 8 fmptd ⊢ φ → F : B ⟶ A
16 11 simprd ⊢ φ → finSupp ∅⁡ G
17 16 fsuppimpd ⊢ φ → G supp ∅ ∈ Fin
18 snfi ⊢ X ∈ Fin
19 unfi ⊢ G supp ∅ ∈ Fin ∧ X ∈ Fin → supp ∅⁡ G ∪ X ∈ Fin
20 17 18 19 sylancl ⊢ φ → supp ∅⁡ G ∪ X ∈ Fin
21 eqeq1 ⊢ t = k → t = X ↔ k = X
22 fveq2 ⊢ t = k → G ⁡ t = G ⁡ k
23 21 22 ifbieq2d ⊢ t = k → if t = X Y G ⁡ t = if k = X Y G ⁡ k
24 eldifi ⊢ k ∈ B ∖ supp ∅⁡ G ∪ X → k ∈ B
25 24 adantl ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → k ∈ B
26 6 adantr ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → Y ∈ A
27 fvex ⊢ G ⁡ k ∈ V
28 ifexg ⊢ Y ∈ A ∧ G ⁡ k ∈ V → if k = X Y G ⁡ k ∈ V
29 26 27 28 sylancl ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → if k = X Y G ⁡ k ∈ V
30 8 23 25 29 fvmptd3 ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → F ⁡ k = if k = X Y G ⁡ k
31 eldifn ⊢ k ∈ B ∖ supp ∅⁡ G ∪ X → ¬ k ∈ supp ∅⁡ G ∪ X
32 31 adantl ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → ¬ k ∈ supp ∅⁡ G ∪ X
33 velsn ⊢ k ∈ X ↔ k = X
34 elun2 ⊢ k ∈ X → k ∈ supp ∅⁡ G ∪ X
35 33 34 sylbir ⊢ k = X → k ∈ supp ∅⁡ G ∪ X
36 32 35 nsyl ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → ¬ k = X
37 36 iffalsed ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → if k = X Y G ⁡ k = G ⁡ k
38 ssun1 ⊢ G supp ∅ ⊆ supp ∅⁡ G ∪ X
39 sscon ⊢ G supp ∅ ⊆ supp ∅⁡ G ∪ X → B ∖ supp ∅⁡ G ∪ X ⊆ B ∖ supp ∅⁡ G
40 38 39 ax-mp ⊢ B ∖ supp ∅⁡ G ∪ X ⊆ B ∖ supp ∅⁡ G
41 40 sseli ⊢ k ∈ B ∖ supp ∅⁡ G ∪ X → k ∈ B ∖ supp ∅⁡ G
42 ssidd ⊢ φ → G supp ∅ ⊆ G supp ∅
43 0ex ⊢ ∅ ∈ V
44 43 a1i ⊢ φ → ∅ ∈ V
45 12 42 3 44 suppssr ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G → G ⁡ k = ∅
46 41 45 sylan2 ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → G ⁡ k = ∅
47 30 37 46 3eqtrd ⊢ φ ∧ k ∈ B ∖ supp ∅⁡ G ∪ X → F ⁡ k = ∅
48 15 47 suppss ⊢ φ → F supp ∅ ⊆ supp ∅⁡ G ∪ X
49 20 48 ssfid ⊢ φ → F supp ∅ ∈ Fin
50 8 funmpt2 ⊢ Fun ⁡ F
51 mptexg ⊢ B ∈ On → t ∈ B ⟼ if t = X Y G ⁡ t ∈ V
52 8 51 eqeltrid ⊢ B ∈ On → F ∈ V
53 3 52 syl ⊢ φ → F ∈ V
54 funisfsupp ⊢ Fun ⁡ F ∧ F ∈ V ∧ ∅ ∈ V → finSupp ∅⁡ F ↔ F supp ∅ ∈ Fin
55 50 53 44 54 mp3an2i ⊢ φ → finSupp ∅⁡ F ↔ F supp ∅ ∈ Fin
56 49 55 mpbird ⊢ φ → finSupp ∅⁡ F
57 1 2 3 cantnfs ⊢ φ → F ∈ S ↔ F : B ⟶ A ∧ finSupp ∅⁡ F
58 15 56 57 mpbir2and ⊢ φ → F ∈ S