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=domACNFB
cantnfs.a φAOn
cantnfs.b φBOn
cantnfrescl.d φDOn
cantnfrescl.b φBD
cantnfrescl.x φnDBX=
cantnfrescl.a φA
cantnfrescl.t T=domACNFD
Assertion cantnfrescl φnBXSnDXT

Proof

Step Hyp Ref Expression
1 cantnfs.s S=domACNFB
2 cantnfs.a φAOn
3 cantnfs.b φBOn
4 cantnfrescl.d φDOn
5 cantnfrescl.b φBD
6 cantnfrescl.x φnDBX=
7 cantnfrescl.a φA
8 cantnfrescl.t T=domACNFD
9 7 adantr φnDBA
10 6 9 eqeltrd φnDBXA
11 10 ralrimiva φnDBXA
12 5 11 raldifeq φnBXAnDXA
13 eqid nBX=nBX
14 13 fmpt nBXAnBX:BA
15 eqid nDX=nDX
16 15 fmpt nDXAnDX:DA
17 12 14 16 3bitr3g φnBX:BAnDX:DA
18 3 mptexd φnBXV
19 funmpt FunnBX
20 19 a1i φFunnBX
21 4 mptexd φnDXV
22 funmpt FunnDX
23 21 22 jctir φnDXVFunnDX
24 18 20 23 jca31 φnBXVFunnBXnDXVFunnDX
25 4 5 6 extmptsuppeq φnBXsupp=nDXsupp
26 suppeqfsuppbi nBXVFunnBXnDXVFunnDXnBXsupp=nDXsuppfinSuppnBXfinSuppnDX
27 24 25 26 sylc φfinSuppnBXfinSuppnDX
28 17 27 anbi12d φnBX:BAfinSuppnBXnDX:DAfinSuppnDX
29 1 2 3 cantnfs φnBXSnBX:BAfinSuppnBX
30 8 2 4 cantnfs φnDXTnDX:DAfinSuppnDX
31 28 29 30 3bitr4d φnBXSnDXT