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 ffvelrnda ( ( 𝜑𝑡𝐵 ) → ( 𝐺𝑡 ) ∈ 𝐴 )
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 ( 𝜑𝐹𝑆 )