Metamath Proof Explorer


Theorem 2ndpreima

Description: The preimage by 2nd is an 'horizontal band'. (Contributed by Thierry Arnoux, 13-Oct-2017)

Ref Expression
Assertion 2ndpreima A C 2 nd B × C -1 A = B × A

Proof

Step Hyp Ref Expression
1 elxp7 w B × C w V × V 1 st w B 2 nd w C
2 1 anbi1i w B × C 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
3 ssel A C 2 nd w A 2 nd w C
4 3 pm4.71rd A C 2 nd w A 2 nd w C 2 nd w A
5 4 anbi2d A C w V × V 1 st w B 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
6 anass w V × V 1 st w B 2 nd w C 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
7 6 bicomi w V × V 1 st w B 2 nd w C 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
8 7 a1i A C w V × V 1 st w B 2 nd w C 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
9 anass w V × V 1 st w B 2 nd w C w V × V 1 st w B 2 nd w C
10 9 anbi1i w V × V 1 st w B 2 nd w C 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
11 10 a1i A C w V × V 1 st w B 2 nd w C 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
12 5 8 11 3bitrd A C w V × V 1 st w B 2 nd w A w V × V 1 st w B 2 nd w C 2 nd w A
13 2 12 bitr4id A C w B × C 2 nd w A w V × V 1 st w B 2 nd w A
14 ancom w B × C 2 nd w A 2 nd w A w B × C
15 anass w V × V 1 st w B 2 nd w A w V × V 1 st w B 2 nd w A
16 13 14 15 3bitr3g A C 2 nd w A w B × C w V × V 1 st w B 2 nd w A
17 cnvresima 2 nd B × C -1 A = 2 nd -1 A B × C
18 17 eleq2i w 2 nd B × C -1 A w 2 nd -1 A B × C
19 elin w 2 nd -1 A B × C w 2 nd -1 A w B × C
20 vex w V
21 fo2nd 2 nd : V onto V
22 fofn 2 nd : V onto V 2 nd Fn V
23 elpreima 2 nd Fn V w 2 nd -1 A w V 2 nd w A
24 21 22 23 mp2b w 2 nd -1 A w V 2 nd w A
25 20 24 mpbiran w 2 nd -1 A 2 nd w A
26 25 anbi1i w 2 nd -1 A w B × C 2 nd w A w B × C
27 18 19 26 3bitri w 2 nd B × C -1 A 2 nd w A w B × C
28 elxp7 w B × A w V × V 1 st w B 2 nd w A
29 16 27 28 3bitr4g A C w 2 nd B × C -1 A w B × A
30 29 eqrdv A C 2 nd B × C -1 A = B × A