Metamath Proof Explorer

Theorem cantnfrescl

Description: A function is finitely supported from B to A iff the extended function is finitely supported from D to A . (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfrescl.d 
|- ( ph -> D e. On )
cantnfrescl.b 
|- ( ph -> B C_ D )
cantnfrescl.x 
|- ( ( ph /\ n e. ( D \ B ) ) -> X = (/) )
cantnfrescl.a 
|- ( ph -> (/) e. A )
cantnfrescl.t 
|- T = dom ( A CNF D )
Assertion cantnfrescl 
|- ( ph -> ( ( n e. B |-> X ) e. S <-> ( n e. D |-> X ) e. T ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 cantnfrescl.d 
 |-  ( ph -> D e. On )
5 cantnfrescl.b 
 |-  ( ph -> B C_ D )
6 cantnfrescl.x 
 |-  ( ( ph /\ n e. ( D \ B ) ) -> X = (/) )
7 cantnfrescl.a 
 |-  ( ph -> (/) e. A )
8 cantnfrescl.t 
 |-  T = dom ( A CNF D )
9 7 adantr 
 |-  ( ( ph /\ n e. ( D \ B ) ) -> (/) e. A )
10 6 9 eqeltrd 
 |-  ( ( ph /\ n e. ( D \ B ) ) -> X e. A )
11 10 ralrimiva 
 |-  ( ph -> A. n e. ( D \ B ) X e. A )
12 5 11 raldifeq 
 |-  ( ph -> ( A. n e. B X e. A <-> A. n e. D X e. A ) )
13 eqid 
 |-  ( n e. B |-> X ) = ( n e. B |-> X )
14 13 fmpt 
 |-  ( A. n e. B X e. A <-> ( n e. B |-> X ) : B --> A )
15 eqid 
 |-  ( n e. D |-> X ) = ( n e. D |-> X )
16 15 fmpt 
 |-  ( A. n e. D X e. A <-> ( n e. D |-> X ) : D --> A )
17 12 14 16 3bitr3g 
 |-  ( ph -> ( ( n e. B |-> X ) : B --> A <-> ( n e. D |-> X ) : D --> A ) )
18 3 mptexd 
 |-  ( ph -> ( n e. B |-> X ) e. _V )
19 funmpt 
 |-  Fun ( n e. B |-> X )
20 19 a1i 
 |-  ( ph -> Fun ( n e. B |-> X ) )
21 4 mptexd 
 |-  ( ph -> ( n e. D |-> X ) e. _V )
22 funmpt 
 |-  Fun ( n e. D |-> X )
23 21 22 jctir 
 |-  ( ph -> ( ( n e. D |-> X ) e. _V /\ Fun ( n e. D |-> X ) ) )
24 18 20 23 jca31 
 |-  ( ph -> ( ( ( n e. B |-> X ) e. _V /\ Fun ( n e. B |-> X ) ) /\ ( ( n e. D |-> X ) e. _V /\ Fun ( n e. D |-> X ) ) ) )
25 4 5 6 extmptsuppeq 
 |-  ( ph -> ( ( n e. B |-> X ) supp (/) ) = ( ( n e. D |-> X ) supp (/) ) )
26 suppeqfsuppbi 
 |-  ( ( ( ( n e. B |-> X ) e. _V /\ Fun ( n e. B |-> X ) ) /\ ( ( n e. D |-> X ) e. _V /\ Fun ( n e. D |-> X ) ) ) -> ( ( ( n e. B |-> X ) supp (/) ) = ( ( n e. D |-> X ) supp (/) ) -> ( ( n e. B |-> X ) finSupp (/) <-> ( n e. D |-> X ) finSupp (/) ) ) )
27 24 25 26 sylc 
 |-  ( ph -> ( ( n e. B |-> X ) finSupp (/) <-> ( n e. D |-> X ) finSupp (/) ) )
28 17 27 anbi12d 
 |-  ( ph -> ( ( ( n e. B |-> X ) : B --> A /\ ( n e. B |-> X ) finSupp (/) ) <-> ( ( n e. D |-> X ) : D --> A /\ ( n e. D |-> X ) finSupp (/) ) ) )
29 1 2 3 cantnfs 
 |-  ( ph -> ( ( n e. B |-> X ) e. S <-> ( ( n e. B |-> X ) : B --> A /\ ( n e. B |-> X ) finSupp (/) ) ) )
30 8 2 4 cantnfs 
 |-  ( ph -> ( ( n e. D |-> X ) e. T <-> ( ( n e. D |-> X ) : D --> A /\ ( n e. D |-> X ) finSupp (/) ) ) )
31 28 29 30 3bitr4d 
 |-  ( ph -> ( ( n e. B |-> X ) e. S <-> ( n e. D |-> X ) e. T ) )