Metamath Proof Explorer


Theorem fo1stres

Description: Onto mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 14-Dec-2008)

Ref Expression
Assertion fo1stres B 1 st A × B : A × B onto A

Proof

Step Hyp Ref Expression
1 n0 B y y B
2 opelxp x y A × B x A y B
3 fvres x y A × B 1 st A × B x y = 1 st x y
4 vex x V
5 vex y V
6 4 5 op1st 1 st x y = x
7 3 6 eqtr2di x y A × B x = 1 st A × B x y
8 f1stres 1 st A × B : A × B A
9 ffn 1 st A × B : A × B A 1 st A × B Fn A × B
10 8 9 ax-mp 1 st A × B Fn A × B
11 fnfvelrn 1 st A × B Fn A × B x y A × B 1 st A × B x y ran 1 st A × B
12 10 11 mpan x y A × B 1 st A × B x y ran 1 st A × B
13 7 12 eqeltrd x y A × B x ran 1 st A × B
14 2 13 sylbir x A y B x ran 1 st A × B
15 14 expcom y B x A x ran 1 st A × B
16 15 exlimiv y y B x A x ran 1 st A × B
17 1 16 sylbi B x A x ran 1 st A × B
18 17 ssrdv B A ran 1 st A × B
19 frn 1 st A × B : A × B A ran 1 st A × B A
20 8 19 ax-mp ran 1 st A × B A
21 18 20 jctil B ran 1 st A × B A A ran 1 st A × B
22 eqss ran 1 st A × B = A ran 1 st A × B A A ran 1 st A × B
23 21 22 sylibr B ran 1 st A × B = A
24 23 8 jctil B 1 st A × B : A × B A ran 1 st A × B = A
25 dffo2 1 st A × B : A × B onto A 1 st A × B : A × B A ran 1 st A × B = A
26 24 25 sylibr B 1 st A × B : A × B onto A