Metamath Proof Explorer


Theorem fmucndlem

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

Ref Expression
Assertion fmucndlem F Fn X A X x X , y X F x F y A × A = F A × F A

Proof

Step Hyp Ref Expression
1 df-ima x X , y X F x F y A × A = ran x X , y X F x F y A × A
2 simpr F Fn X A X A X
3 resmpo A X A X x X , y X F x F y A × A = x A , y A F x F y
4 2 3 sylancom F Fn X A X x X , y X F x F y A × A = x A , y A F x F y
5 4 rneqd F Fn X A X ran x X , y X F x F y A × A = ran x A , y A F x F y
6 1 5 syl5eq F Fn X A X x X , y X F x F y A × A = ran x A , y A F x F y
7 vex x V
8 vex y V
9 7 8 op1std p = x y 1 st p = x
10 9 fveq2d p = x y F 1 st p = F x
11 7 8 op2ndd p = x y 2 nd p = y
12 11 fveq2d p = x y F 2 nd p = F y
13 10 12 opeq12d p = x y F 1 st p F 2 nd p = F x F y
14 13 mpompt p A × A F 1 st p F 2 nd p = x A , y A F x F y
15 14 eqcomi x A , y A F x F y = p A × A F 1 st p F 2 nd p
16 15 rneqi ran x A , y A F x F y = ran p A × A F 1 st p F 2 nd p
17 fvexd p A × A F 1 st p V
18 fvexd p A × A F 2 nd p V
19 16 17 18 fliftrel ran x A , y A F x F y V × V
20 19 mptru ran x A , y A F x F y V × V
21 20 sseli p ran x A , y A F x F y p V × V
22 21 adantl F Fn X A X p ran x A , y A F x F y p V × V
23 xpss F A × F A V × V
24 23 sseli p F A × F A p V × V
25 24 adantl F Fn X A X p F A × F A p V × V
26 eqid x A , y A F x F y = x A , y A F x F y
27 opex F x F y V
28 26 27 elrnmpo 1 st p 2 nd p ran x A , y A F x F y x A y A 1 st p 2 nd p = F x F y
29 eqcom 1 st p 2 nd p = F x F y F x F y = 1 st p 2 nd p
30 fvex 1 st p V
31 fvex 2 nd p V
32 30 31 opth2 F x F y = 1 st p 2 nd p F x = 1 st p F y = 2 nd p
33 29 32 bitri 1 st p 2 nd p = F x F y F x = 1 st p F y = 2 nd p
34 33 2rexbii x A y A 1 st p 2 nd p = F x F y x A y A F x = 1 st p F y = 2 nd p
35 reeanv x A y A F x = 1 st p F y = 2 nd p x A F x = 1 st p y A F y = 2 nd p
36 28 34 35 3bitri 1 st p 2 nd p ran x A , y A F x F y x A F x = 1 st p y A F y = 2 nd p
37 fvelimab F Fn X A X 1 st p F A x A F x = 1 st p
38 fvelimab F Fn X A X 2 nd p F A y A F y = 2 nd p
39 37 38 anbi12d F Fn X A X 1 st p F A 2 nd p F A x A F x = 1 st p y A F y = 2 nd p
40 36 39 bitr4id F Fn X A X 1 st p 2 nd p ran x A , y A F x F y 1 st p F A 2 nd p F A
41 opelxp 1 st p 2 nd p F A × F A 1 st p F A 2 nd p F A
42 40 41 bitr4di F Fn X A X 1 st p 2 nd p ran x A , y A F x F y 1 st p 2 nd p F A × F A
43 42 adantr F Fn X A X p V × V 1 st p 2 nd p ran x A , y A F x F y 1 st p 2 nd p F A × F A
44 1st2nd2 p V × V p = 1 st p 2 nd p
45 44 adantl F Fn X A X p V × V p = 1 st p 2 nd p
46 45 eleq1d F Fn X A X p V × V p ran x A , y A F x F y 1 st p 2 nd p ran x A , y A F x F y
47 45 eleq1d F Fn X A X p V × V p F A × F A 1 st p 2 nd p F A × F A
48 43 46 47 3bitr4d F Fn X A X p V × V p ran x A , y A F x F y p F A × F A
49 22 25 48 eqrdav F Fn X A X ran x A , y A F x F y = F A × F A
50 6 49 eqtrd F Fn X A X x X , y X F x F y A × A = F A × F A