Metamath Proof Explorer


Theorem 2ndimaxp

Description: Image of a cartesian product by 2nd . (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Assertion 2ndimaxp A 2 nd A × B = B

Proof

Step Hyp Ref Expression
1 ima0 2 nd =
2 xpeq2 B = A × B = A ×
3 xp0 A × =
4 2 3 eqtrdi B = A × B =
5 4 imaeq2d B = 2 nd A × B = 2 nd
6 id B = B =
7 1 5 6 3eqtr4a B = 2 nd A × B = B
8 7 adantl A B = 2 nd A × B = B
9 xpnz A B A × B
10 fo2nd 2 nd : V onto V
11 fofn 2 nd : V onto V 2 nd Fn V
12 10 11 mp1i A × B 2 nd Fn V
13 ssv A × B V
14 13 a1i A × B A × B V
15 12 14 fvelimabd A × B y 2 nd A × B p A × B 2 nd p = y
16 9 15 sylbi A B y 2 nd A × B p A × B 2 nd p = y
17 simpr A B p A × B 2 nd p = y 2 nd p = y
18 xp2nd p A × B 2 nd p B
19 18 ad2antlr A B p A × B 2 nd p = y 2 nd p B
20 17 19 eqeltrrd A B p A × B 2 nd p = y y B
21 20 r19.29an A B p A × B 2 nd p = y y B
22 n0 A x x A
23 22 biimpi A x x A
24 23 ad2antrr A B y B x x A
25 opelxpi x A y B x y A × B
26 25 ancoms y B x A x y A × B
27 26 adantll A B y B x A x y A × B
28 fveqeq2 p = x y 2 nd p = y 2 nd x y = y
29 28 adantl A B y B x A p = x y 2 nd p = y 2 nd x y = y
30 vex x V
31 vex y V
32 30 31 op2nd 2 nd x y = y
33 32 a1i A B y B x A 2 nd x y = y
34 27 29 33 rspcedvd A B y B x A p A × B 2 nd p = y
35 24 34 exlimddv A B y B p A × B 2 nd p = y
36 21 35 impbida A B p A × B 2 nd p = y y B
37 16 36 bitrd A B y 2 nd A × B y B
38 37 eqrdv A B 2 nd A × B = B
39 8 38 pm2.61dane A 2 nd A × B = B