Metamath Proof Explorer

Theorem mptiffisupp

Description: Conditions for a mapping function defined with a conditional to have finite support. (Contributed by Thierry Arnoux, 20-Feb-2025)

Ref Expression
Hypotheses mptiffisupp.f 
|- F = ( x e. A |-> if ( x e. B , C , Z ) )
mptiffisupp.a 
|- ( ph -> A e. U )
mptiffisupp.b 
|- ( ph -> B e. Fin )
mptiffisupp.c 
|- ( ( ph /\ x e. B ) -> C e. V )
mptiffisupp.z 
|- ( ph -> Z e. W )
Assertion mptiffisupp 
|- ( ph -> F finSupp Z )

Proof

Step Hyp Ref Expression
1 mptiffisupp.f 
 |-  F = ( x e. A |-> if ( x e. B , C , Z ) )
2 mptiffisupp.a 
 |-  ( ph -> A e. U )
3 mptiffisupp.b 
 |-  ( ph -> B e. Fin )
4 mptiffisupp.c 
 |-  ( ( ph /\ x e. B ) -> C e. V )
5 mptiffisupp.z 
 |-  ( ph -> Z e. W )
6 2 mptexd 
 |-  ( ph -> ( x e. A |-> if ( x e. B , C , Z ) ) e. _V )
7 1 6 eqeltrid 
 |-  ( ph -> F e. _V )
8 1 funmpt2 
 |-  Fun F
9 8 a1i 
 |-  ( ph -> Fun F )
10 partfun 
 |-  ( x e. A |-> if ( x e. B , C , Z ) ) = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> Z ) )
11 1 10 eqtri 
 |-  F = ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> Z ) )
12 11 oveq1i 
 |-  ( F supp Z ) = ( ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> Z ) ) supp Z )
13 inss2 
 |-  ( A i^i B ) C_ B
14 13 a1i 
 |-  ( ph -> ( A i^i B ) C_ B )
15 14 sselda 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> x e. B )
16 15 4 syldan 
 |-  ( ( ph /\ x e. ( A i^i B ) ) -> C e. V )
17 16 fmpttd 
 |-  ( ph -> ( x e. ( A i^i B ) |-> C ) : ( A i^i B ) --> V )
18 incom 
 |-  ( B i^i A ) = ( A i^i B )
19 infi 
 |-  ( B e. Fin -> ( B i^i A ) e. Fin )
20 3 19 syl 
 |-  ( ph -> ( B i^i A ) e. Fin )
21 18 20 eqeltrrid 
 |-  ( ph -> ( A i^i B ) e. Fin )
22 17 21 5 fidmfisupp 
 |-  ( ph -> ( x e. ( A i^i B ) |-> C ) finSupp Z )
23 difexg 
 |-  ( A e. U -> ( A \ B ) e. _V )
24 mptexg 
 |-  ( ( A \ B ) e. _V -> ( x e. ( A \ B ) |-> Z ) e. _V )
25 2 23 24 3syl 
 |-  ( ph -> ( x e. ( A \ B ) |-> Z ) e. _V )
26 funmpt 
 |-  Fun ( x e. ( A \ B ) |-> Z )
27 26 a1i 
 |-  ( ph -> Fun ( x e. ( A \ B ) |-> Z ) )
28 supppreima 
 |-  ( ( Fun ( x e. ( A \ B ) |-> Z ) /\ ( x e. ( A \ B ) |-> Z ) e. _V /\ Z e. W ) -> ( ( x e. ( A \ B ) |-> Z ) supp Z ) = ( `' ( x e. ( A \ B ) |-> Z ) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) )
29 26 25 5 28 mp3an2i 
 |-  ( ph -> ( ( x e. ( A \ B ) |-> Z ) supp Z ) = ( `' ( x e. ( A \ B ) |-> Z ) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) )
30 simpr 
 |-  ( ( ph /\ ( A \ B ) = (/) ) -> ( A \ B ) = (/) )
31 30 mpteq1d 
 |-  ( ( ph /\ ( A \ B ) = (/) ) -> ( x e. ( A \ B ) |-> Z ) = ( x e. (/) |-> Z ) )
32 mpt0 
 |-  ( x e. (/) |-> Z ) = (/)
33 31 32 eqtrdi 
 |-  ( ( ph /\ ( A \ B ) = (/) ) -> ( x e. ( A \ B ) |-> Z ) = (/) )
34 33 cnveqd 
 |-  ( ( ph /\ ( A \ B ) = (/) ) -> `' ( x e. ( A \ B ) |-> Z ) = `' (/) )
35 cnv0 
 |-  `' (/) = (/)
36 34 35 eqtrdi 
 |-  ( ( ph /\ ( A \ B ) = (/) ) -> `' ( x e. ( A \ B ) |-> Z ) = (/) )
37 36 imaeq1d 
 |-  ( ( ph /\ ( A \ B ) = (/) ) -> ( `' ( x e. ( A \ B ) |-> Z ) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) = ( (/) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) )
38 0ima 
 |-  ( (/) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) = (/)
39 37 38 eqtrdi 
 |-  ( ( ph /\ ( A \ B ) = (/) ) -> ( `' ( x e. ( A \ B ) |-> Z ) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) = (/) )
40 eqid 
 |-  ( x e. ( A \ B ) |-> Z ) = ( x e. ( A \ B ) |-> Z )
41 simpr 
 |-  ( ( ph /\ ( A \ B ) =/= (/) ) -> ( A \ B ) =/= (/) )
42 40 41 rnmptc 
 |-  ( ( ph /\ ( A \ B ) =/= (/) ) -> ran ( x e. ( A \ B ) |-> Z ) = { Z } )
43 42 difeq1d 
 |-  ( ( ph /\ ( A \ B ) =/= (/) ) -> ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) = ( { Z } \ { Z } ) )
44 difid 
 |-  ( { Z } \ { Z } ) = (/)
45 43 44 eqtrdi 
 |-  ( ( ph /\ ( A \ B ) =/= (/) ) -> ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) = (/) )
46 45 imaeq2d 
 |-  ( ( ph /\ ( A \ B ) =/= (/) ) -> ( `' ( x e. ( A \ B ) |-> Z ) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) = ( `' ( x e. ( A \ B ) |-> Z ) " (/) ) )
47 ima0 
 |-  ( `' ( x e. ( A \ B ) |-> Z ) " (/) ) = (/)
48 46 47 eqtrdi 
 |-  ( ( ph /\ ( A \ B ) =/= (/) ) -> ( `' ( x e. ( A \ B ) |-> Z ) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) = (/) )
49 39 48 pm2.61dane 
 |-  ( ph -> ( `' ( x e. ( A \ B ) |-> Z ) " ( ran ( x e. ( A \ B ) |-> Z ) \ { Z } ) ) = (/) )
50 29 49 eqtrd 
 |-  ( ph -> ( ( x e. ( A \ B ) |-> Z ) supp Z ) = (/) )
51 0fin 
 |-  (/) e. Fin
52 50 51 eqeltrdi 
 |-  ( ph -> ( ( x e. ( A \ B ) |-> Z ) supp Z ) e. Fin )
53 25 5 27 52 isfsuppd 
 |-  ( ph -> ( x e. ( A \ B ) |-> Z ) finSupp Z )
54 22 53 fsuppun 
 |-  ( ph -> ( ( ( x e. ( A i^i B ) |-> C ) u. ( x e. ( A \ B ) |-> Z ) ) supp Z ) e. Fin )
55 12 54 eqeltrid 
 |-  ( ph -> ( F supp Z ) e. Fin )
56 7 5 9 55 isfsuppd 
 |-  ( ph -> F finSupp Z )