Metamath Proof Explorer


Theorem fodomfiOLD

Description: Obsolete version of fodomfi as of 20-Jun-2025. (Contributed by NM, 23-Mar-2006) (Proof shortened by Mario Carneiro, 16-Nov-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fodomfiOLD A Fin F : A onto B B A

Proof

Step Hyp Ref Expression
1 foima F : A onto B F A = B
2 1 adantl A Fin F : A onto B F A = B
3 imaeq2 x = F x = F
4 ima0 F =
5 3 4 eqtrdi x = F x =
6 id x = x =
7 5 6 breq12d x = F x x
8 7 imbi2d x = F Fn A F x x F Fn A
9 imaeq2 x = y F x = F y
10 id x = y x = y
11 9 10 breq12d x = y F x x F y y
12 11 imbi2d x = y F Fn A F x x F Fn A F y y
13 imaeq2 x = y z F x = F y z
14 id x = y z x = y z
15 13 14 breq12d x = y z F x x F y z y z
16 15 imbi2d x = y z F Fn A F x x F Fn A F y z y z
17 imaeq2 x = A F x = F A
18 id x = A x = A
19 17 18 breq12d x = A F x x F A A
20 19 imbi2d x = A F Fn A F x x F Fn A F A A
21 0ex V
22 21 0dom
23 22 a1i F Fn A
24 fnfun F Fn A Fun F
25 24 ad2antrl y Fin ¬ z y F Fn A F y y Fun F
26 funressn Fun F F z z F z
27 rnss F z z F z ran F z ran z F z
28 25 26 27 3syl y Fin ¬ z y F Fn A F y y ran F z ran z F z
29 df-ima F z = ran F z
30 vex z V
31 30 rnsnop ran z F z = F z
32 31 eqcomi F z = ran z F z
33 28 29 32 3sstr4g y Fin ¬ z y F Fn A F y y F z F z
34 snex F z V
35 ssexg F z F z F z V F z V
36 33 34 35 sylancl y Fin ¬ z y F Fn A F y y F z V
37 fvi F z V I F z = F z
38 36 37 syl y Fin ¬ z y F Fn A F y y I F z = F z
39 38 uneq2d y Fin ¬ z y F Fn A F y y F y I F z = F y F z
40 imaundi F y z = F y F z
41 39 40 eqtr4di y Fin ¬ z y F Fn A F y y F y I F z = F y z
42 simprr y Fin ¬ z y F Fn A F y y F y y
43 ssdomg F z V F z F z F z F z
44 34 33 43 mpsyl y Fin ¬ z y F Fn A F y y F z F z
45 fvex F z V
46 45 ensn1 F z 1 𝑜
47 30 ensn1 z 1 𝑜
48 46 47 entr4i F z z
49 domentr F z F z F z z F z z
50 44 48 49 sylancl y Fin ¬ z y F Fn A F y y F z z
51 38 50 eqbrtrd y Fin ¬ z y F Fn A F y y I F z z
52 simplr y Fin ¬ z y F Fn A F y y ¬ z y
53 disjsn y z = ¬ z y
54 52 53 sylibr y Fin ¬ z y F Fn A F y y y z =
55 undom F y y I F z z y z = F y I F z y z
56 42 51 54 55 syl21anc y Fin ¬ z y F Fn A F y y F y I F z y z
57 41 56 eqbrtrrd y Fin ¬ z y F Fn A F y y F y z y z
58 57 exp32 y Fin ¬ z y F Fn A F y y F y z y z
59 58 a2d y Fin ¬ z y F Fn A F y y F Fn A F y z y z
60 8 12 16 20 23 59 findcard2s A Fin F Fn A F A A
61 fofn F : A onto B F Fn A
62 60 61 impel A Fin F : A onto B F A A
63 2 62 eqbrtrrd A Fin F : A onto B B A