Metamath Proof Explorer


Theorem fmucndlem

Description: Lemma for fmucnd . (Contributed by Thierry Arnoux, 19-Nov-2017)

Ref Expression
Assertion fmucndlem FFnXAXxX,yXFxFyA×A=FA×FA

Proof

Step Hyp Ref Expression
1 df-ima xX,yXFxFyA×A=ranxX,yXFxFyA×A
2 simpr FFnXAXAX
3 resmpo AXAXxX,yXFxFyA×A=xA,yAFxFy
4 2 3 sylancom FFnXAXxX,yXFxFyA×A=xA,yAFxFy
5 4 rneqd FFnXAXranxX,yXFxFyA×A=ranxA,yAFxFy
6 1 5 eqtrid FFnXAXxX,yXFxFyA×A=ranxA,yAFxFy
7 vex xV
8 vex yV
9 7 8 op1std p=xy1stp=x
10 9 fveq2d p=xyF1stp=Fx
11 7 8 op2ndd p=xy2ndp=y
12 11 fveq2d p=xyF2ndp=Fy
13 10 12 opeq12d p=xyF1stpF2ndp=FxFy
14 13 mpompt pA×AF1stpF2ndp=xA,yAFxFy
15 14 eqcomi xA,yAFxFy=pA×AF1stpF2ndp
16 15 rneqi ranxA,yAFxFy=ranpA×AF1stpF2ndp
17 fvexd pA×AF1stpV
18 fvexd pA×AF2ndpV
19 16 17 18 fliftrel ranxA,yAFxFyV×V
20 19 mptru ranxA,yAFxFyV×V
21 20 sseli pranxA,yAFxFypV×V
22 21 adantl FFnXAXpranxA,yAFxFypV×V
23 xpss FA×FAV×V
24 23 sseli pFA×FApV×V
25 24 adantl FFnXAXpFA×FApV×V
26 eqid xA,yAFxFy=xA,yAFxFy
27 opex FxFyV
28 26 27 elrnmpo 1stp2ndpranxA,yAFxFyxAyA1stp2ndp=FxFy
29 eqcom 1stp2ndp=FxFyFxFy=1stp2ndp
30 fvex 1stpV
31 fvex 2ndpV
32 30 31 opth2 FxFy=1stp2ndpFx=1stpFy=2ndp
33 29 32 bitri 1stp2ndp=FxFyFx=1stpFy=2ndp
34 33 2rexbii xAyA1stp2ndp=FxFyxAyAFx=1stpFy=2ndp
35 reeanv xAyAFx=1stpFy=2ndpxAFx=1stpyAFy=2ndp
36 28 34 35 3bitri 1stp2ndpranxA,yAFxFyxAFx=1stpyAFy=2ndp
37 fvelimab FFnXAX1stpFAxAFx=1stp
38 fvelimab FFnXAX2ndpFAyAFy=2ndp
39 37 38 anbi12d FFnXAX1stpFA2ndpFAxAFx=1stpyAFy=2ndp
40 36 39 bitr4id FFnXAX1stp2ndpranxA,yAFxFy1stpFA2ndpFA
41 opelxp 1stp2ndpFA×FA1stpFA2ndpFA
42 40 41 bitr4di FFnXAX1stp2ndpranxA,yAFxFy1stp2ndpFA×FA
43 42 adantr FFnXAXpV×V1stp2ndpranxA,yAFxFy1stp2ndpFA×FA
44 1st2nd2 pV×Vp=1stp2ndp
45 44 adantl FFnXAXpV×Vp=1stp2ndp
46 45 eleq1d FFnXAXpV×VpranxA,yAFxFy1stp2ndpranxA,yAFxFy
47 45 eleq1d FFnXAXpV×VpFA×FA1stp2ndpFA×FA
48 43 46 47 3bitr4d FFnXAXpV×VpranxA,yAFxFypFA×FA
49 22 25 48 eqrdav FFnXAXranxA,yAFxFy=FA×FA
50 6 49 eqtrd FFnXAXxX,yXFxFyA×A=FA×FA