Metamath Proof Explorer


Theorem dffo3f

Description: An onto mapping expressed in terms of function values. As dffo3 but with less disjoint vars constraints. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis dffo3f.1 _ x F
Assertion dffo3f F : A onto B F : A B y B x A y = F x

Proof

Step Hyp Ref Expression
1 dffo3f.1 _ x F
2 dffo2 F : A onto B F : A B ran F = B
3 ffn F : A B F Fn A
4 fnrnfv F Fn A ran F = y | w A y = F w
5 nfcv _ x w
6 1 5 nffv _ x F w
7 6 nfeq2 x y = F w
8 nfv w y = F x
9 fveq2 w = x F w = F x
10 9 eqeq2d w = x y = F w y = F x
11 7 8 10 cbvrexw w A y = F w x A y = F x
12 11 abbii y | w A y = F w = y | x A y = F x
13 4 12 syl6eq F Fn A ran F = y | x A y = F x
14 13 eqeq1d F Fn A ran F = B y | x A y = F x = B
15 3 14 syl F : A B ran F = B y | x A y = F x = B
16 nfcv _ x A
17 nfcv _ x B
18 1 16 17 nff x F : A B
19 nfv x y B
20 simpr F : A B x A y = F x y = F x
21 ffvelrn F : A B x A F x B
22 21 adantr F : A B x A y = F x F x B
23 20 22 eqeltrd F : A B x A y = F x y B
24 18 19 23 rexlimd3 F : A B x A y = F x y B
25 24 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
26 dfbi2 x A y = F x y B x A y = F x y B y B x A y = F x
27 25 26 syl6rbbr F : A B x A y = F x y B y B x A y = F x
28 27 albidv F : A B y x A y = F x y B y y B x A y = F x
29 abeq1 y | x A y = F x = B y x A y = F x y B
30 df-ral y B x A y = F x y y B x A y = F x
31 28 29 30 3bitr4g F : A B y | x A y = F x = B y B x A y = F x
32 15 31 bitrd F : A B ran F = B y B x A y = F x
33 32 pm5.32i F : A B ran F = B F : A B y B x A y = F x
34 2 33 bitri F : A onto B F : A B y B x A y = F x