This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
cantnfp1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
cantnfp1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
cantnfp1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
cantnfp1.s ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝑋 )
cantnfp1.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) )
Assertion cantnfp1lem1 ( 𝜑 → 𝐹 ∈ 𝑆 )

Proof

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