Metamath Proof Explorer


Theorem dffo3

Description: An onto mapping expressed in terms of function values. (Contributed by NM, 29-Oct-2006)

Ref Expression
Assertion dffo3 F : A onto B F : A B y B x A y = F x

Proof

Step Hyp Ref Expression
1 dffo2 F : A onto B F : A B ran F = B
2 ffn F : A B F Fn A
3 fnrnfv F Fn A ran F = y | x A y = F x
4 3 eqeq1d F Fn A ran F = B y | x A y = F x = B
5 2 4 syl F : A B ran F = B y | x A y = F x = B
6 dfbi2 x A y = F x y B x A y = F x y B y B x A y = F x
7 simpr F : A B x A y = F x y = F x
8 ffvelrn F : A B x A F x B
9 8 adantr F : A B x A y = F x F x B
10 7 9 eqeltrd F : A B x A y = F x y B
11 10 rexlimdva2 F : A B x A y = F x y B
12 11 biantrurd F : A B y B x A y = F x x A y = F x y B y B x A y = F x
13 6 12 bitr4id F : A B x A y = F x y B y B x A y = F x
14 13 albidv F : A B y x A y = F x y B y y B x A y = F x
15 abeq1 y | x A y = F x = B y x A y = F x y B
16 df-ral y B x A y = F x y y B x A y = F x
17 14 15 16 3bitr4g F : A B y | x A y = F x = B y B x A y = F x
18 5 17 bitrd F : A B ran F = B y B x A y = F x
19 18 pm5.32i F : A B ran F = B F : A B y B x A y = F x
20 1 19 bitri F : A onto B F : A B y B x A y = F x