Metamath Proof Explorer

Theorem f1oweALT

Description: Alternate proof of f1owe , more direct since not using the isomorphism predicate, but requiring ax-un . (Contributed by NM, 4-Mar-1997) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis f1oweALT.1 
|- R = { <. x , y >. | ( F ` x ) S ( F ` y ) }
Assertion f1oweALT 
|- ( F : A -1-1-onto-> B -> ( S We B -> R We A ) )

Proof

Step Hyp Ref Expression
1 f1oweALT.1 
 |-  R = { <. x , y >. | ( F ` x ) S ( F ` y ) }
2 f1ofo 
 |-  ( F : A -1-1-onto-> B -> F : A -onto-> B )
3 df-fo 
 |-  ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4 freq2 
 |-  ( ran F = B -> ( S Fr ran F <-> S Fr B ) )
5 4 biimprd 
 |-  ( ran F = B -> ( S Fr B -> S Fr ran F ) )
6 df-fn 
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
7 df-fr 
 |-  ( S Fr ran F <-> A. w ( ( w C_ ran F /\ w =/= (/) ) -> E. u e. w A. f e. w -. f S u ) )
8 vex 
 |-  z e. _V
9 8 funimaex 
 |-  ( Fun F -> ( F " z ) e. _V )
10 n0 
 |-  ( z =/= (/) <-> E. w w e. z )
11 funfvima2 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( w e. z -> ( F ` w ) e. ( F " z ) ) )
12 ne0i 
 |-  ( ( F ` w ) e. ( F " z ) -> ( F " z ) =/= (/) )
13 11 12 syl6 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( w e. z -> ( F " z ) =/= (/) ) )
14 13 exlimdv 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( E. w w e. z -> ( F " z ) =/= (/) ) )
15 10 14 syl5bi 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( z =/= (/) -> ( F " z ) =/= (/) ) )
16 15 imp 
 |-  ( ( ( Fun F /\ z C_ dom F ) /\ z =/= (/) ) -> ( F " z ) =/= (/) )
17 imassrn 
 |-  ( F " z ) C_ ran F
18 16 17 jctil 
 |-  ( ( ( Fun F /\ z C_ dom F ) /\ z =/= (/) ) -> ( ( F " z ) C_ ran F /\ ( F " z ) =/= (/) ) )
19 sseq1 
 |-  ( w = ( F " z ) -> ( w C_ ran F <-> ( F " z ) C_ ran F ) )
20 neeq1 
 |-  ( w = ( F " z ) -> ( w =/= (/) <-> ( F " z ) =/= (/) ) )
21 19 20 anbi12d 
 |-  ( w = ( F " z ) -> ( ( w C_ ran F /\ w =/= (/) ) <-> ( ( F " z ) C_ ran F /\ ( F " z ) =/= (/) ) ) )
22 raleq 
 |-  ( w = ( F " z ) -> ( A. f e. w -. f S u <-> A. f e. ( F " z ) -. f S u ) )
23 22 rexeqbi1dv 
 |-  ( w = ( F " z ) -> ( E. u e. w A. f e. w -. f S u <-> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) )
24 21 23 imbi12d 
 |-  ( w = ( F " z ) -> ( ( ( w C_ ran F /\ w =/= (/) ) -> E. u e. w A. f e. w -. f S u ) <-> ( ( ( F " z ) C_ ran F /\ ( F " z ) =/= (/) ) -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) )
25 24 spcgv 
 |-  ( ( F " z ) e. _V -> ( A. w ( ( w C_ ran F /\ w =/= (/) ) -> E. u e. w A. f e. w -. f S u ) -> ( ( ( F " z ) C_ ran F /\ ( F " z ) =/= (/) ) -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) )
26 18 25 syl7 
 |-  ( ( F " z ) e. _V -> ( A. w ( ( w C_ ran F /\ w =/= (/) ) -> E. u e. w A. f e. w -. f S u ) -> ( ( ( Fun F /\ z C_ dom F ) /\ z =/= (/) ) -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) )
27 9 26 syl 
 |-  ( Fun F -> ( A. w ( ( w C_ ran F /\ w =/= (/) ) -> E. u e. w A. f e. w -. f S u ) -> ( ( ( Fun F /\ z C_ dom F ) /\ z =/= (/) ) -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) )
28 7 27 syl5bi 
 |-  ( Fun F -> ( S Fr ran F -> ( ( ( Fun F /\ z C_ dom F ) /\ z =/= (/) ) -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) )
29 28 com23 
 |-  ( Fun F -> ( ( ( Fun F /\ z C_ dom F ) /\ z =/= (/) ) -> ( S Fr ran F -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) )
30 29 expd 
 |-  ( Fun F -> ( ( Fun F /\ z C_ dom F ) -> ( z =/= (/) -> ( S Fr ran F -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) ) )
31 30 anabsi5 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( z =/= (/) -> ( S Fr ran F -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) ) )
32 31 impd 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( ( z =/= (/) /\ S Fr ran F ) -> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) )
33 fores 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( F |` z ) : z -onto-> ( F " z ) )
34 vex 
 |-  v e. _V
35 vex 
 |-  w e. _V
36 fveq2 
 |-  ( x = v -> ( F ` x ) = ( F ` v ) )
37 36 breq1d 
 |-  ( x = v -> ( ( F ` x ) S ( F ` y ) <-> ( F ` v ) S ( F ` y ) ) )
38 fveq2 
 |-  ( y = w -> ( F ` y ) = ( F ` w ) )
39 38 breq2d 
 |-  ( y = w -> ( ( F ` v ) S ( F ` y ) <-> ( F ` v ) S ( F ` w ) ) )
40 34 35 37 39 1 brab 
 |-  ( v R w <-> ( F ` v ) S ( F ` w ) )
41 fvres 
 |-  ( v e. z -> ( ( F |` z ) ` v ) = ( F ` v ) )
42 fvres 
 |-  ( w e. z -> ( ( F |` z ) ` w ) = ( F ` w ) )
43 41 42 breqan12rd 
 |-  ( ( w e. z /\ v e. z ) -> ( ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) <-> ( F ` v ) S ( F ` w ) ) )
44 40 43 bitr4id 
 |-  ( ( w e. z /\ v e. z ) -> ( v R w <-> ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) ) )
45 44 notbid 
 |-  ( ( w e. z /\ v e. z ) -> ( -. v R w <-> -. ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) ) )
46 45 ralbidva 
 |-  ( w e. z -> ( A. v e. z -. v R w <-> A. v e. z -. ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) ) )
47 46 rexbiia 
 |-  ( E. w e. z A. v e. z -. v R w <-> E. w e. z A. v e. z -. ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) )
48 breq1 
 |-  ( ( ( F |` z ) ` v ) = f -> ( ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) <-> f S ( ( F |` z ) ` w ) ) )
49 48 notbid 
 |-  ( ( ( F |` z ) ` v ) = f -> ( -. ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) <-> -. f S ( ( F |` z ) ` w ) ) )
50 49 cbvfo 
 |-  ( ( F |` z ) : z -onto-> ( F " z ) -> ( A. v e. z -. ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) <-> A. f e. ( F " z ) -. f S ( ( F |` z ) ` w ) ) )
51 50 rexbidv 
 |-  ( ( F |` z ) : z -onto-> ( F " z ) -> ( E. w e. z A. v e. z -. ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) <-> E. w e. z A. f e. ( F " z ) -. f S ( ( F |` z ) ` w ) ) )
52 breq2 
 |-  ( ( ( F |` z ) ` w ) = u -> ( f S ( ( F |` z ) ` w ) <-> f S u ) )
53 52 notbid 
 |-  ( ( ( F |` z ) ` w ) = u -> ( -. f S ( ( F |` z ) ` w ) <-> -. f S u ) )
54 53 ralbidv 
 |-  ( ( ( F |` z ) ` w ) = u -> ( A. f e. ( F " z ) -. f S ( ( F |` z ) ` w ) <-> A. f e. ( F " z ) -. f S u ) )
55 54 cbvexfo 
 |-  ( ( F |` z ) : z -onto-> ( F " z ) -> ( E. w e. z A. f e. ( F " z ) -. f S ( ( F |` z ) ` w ) <-> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) )
56 51 55 bitrd 
 |-  ( ( F |` z ) : z -onto-> ( F " z ) -> ( E. w e. z A. v e. z -. ( ( F |` z ) ` v ) S ( ( F |` z ) ` w ) <-> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) )
57 47 56 bitrid 
 |-  ( ( F |` z ) : z -onto-> ( F " z ) -> ( E. w e. z A. v e. z -. v R w <-> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) )
58 33 57 syl 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( E. w e. z A. v e. z -. v R w <-> E. u e. ( F " z ) A. f e. ( F " z ) -. f S u ) )
59 32 58 sylibrd 
 |-  ( ( Fun F /\ z C_ dom F ) -> ( ( z =/= (/) /\ S Fr ran F ) -> E. w e. z A. v e. z -. v R w ) )
60 59 exp4b 
 |-  ( Fun F -> ( z C_ dom F -> ( z =/= (/) -> ( S Fr ran F -> E. w e. z A. v e. z -. v R w ) ) ) )
61 60 com34 
 |-  ( Fun F -> ( z C_ dom F -> ( S Fr ran F -> ( z =/= (/) -> E. w e. z A. v e. z -. v R w ) ) ) )
62 61 com23 
 |-  ( Fun F -> ( S Fr ran F -> ( z C_ dom F -> ( z =/= (/) -> E. w e. z A. v e. z -. v R w ) ) ) )
63 62 imp4a 
 |-  ( Fun F -> ( S Fr ran F -> ( ( z C_ dom F /\ z =/= (/) ) -> E. w e. z A. v e. z -. v R w ) ) )
64 63 alrimdv 
 |-  ( Fun F -> ( S Fr ran F -> A. z ( ( z C_ dom F /\ z =/= (/) ) -> E. w e. z A. v e. z -. v R w ) ) )
65 df-fr 
 |-  ( R Fr dom F <-> A. z ( ( z C_ dom F /\ z =/= (/) ) -> E. w e. z A. v e. z -. v R w ) )
66 64 65 syl6ibr 
 |-  ( Fun F -> ( S Fr ran F -> R Fr dom F ) )
67 freq2 
 |-  ( dom F = A -> ( R Fr dom F <-> R Fr A ) )
68 67 biimpd 
 |-  ( dom F = A -> ( R Fr dom F -> R Fr A ) )
69 66 68 sylan9 
 |-  ( ( Fun F /\ dom F = A ) -> ( S Fr ran F -> R Fr A ) )
70 6 69 sylbi 
 |-  ( F Fn A -> ( S Fr ran F -> R Fr A ) )
71 5 70 sylan9r 
 |-  ( ( F Fn A /\ ran F = B ) -> ( S Fr B -> R Fr A ) )
72 3 71 sylbi 
 |-  ( F : A -onto-> B -> ( S Fr B -> R Fr A ) )
73 2 72 syl 
 |-  ( F : A -1-1-onto-> B -> ( S Fr B -> R Fr A ) )
74 df-f1o 
 |-  ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )
75 fveq2 
 |-  ( x = w -> ( F ` x ) = ( F ` w ) )
76 75 breq1d 
 |-  ( x = w -> ( ( F ` x ) S ( F ` y ) <-> ( F ` w ) S ( F ` y ) ) )
77 fveq2 
 |-  ( y = v -> ( F ` y ) = ( F ` v ) )
78 77 breq2d 
 |-  ( y = v -> ( ( F ` w ) S ( F ` y ) <-> ( F ` w ) S ( F ` v ) ) )
79 35 34 76 78 1 brab 
 |-  ( w R v <-> ( F ` w ) S ( F ` v ) )
80 79 a1i 
 |-  ( ( F : A -1-1-> B /\ ( w e. A /\ v e. A ) ) -> ( w R v <-> ( F ` w ) S ( F ` v ) ) )
81 f1fveq 
 |-  ( ( F : A -1-1-> B /\ ( w e. A /\ v e. A ) ) -> ( ( F ` w ) = ( F ` v ) <-> w = v ) )
82 81 bicomd 
 |-  ( ( F : A -1-1-> B /\ ( w e. A /\ v e. A ) ) -> ( w = v <-> ( F ` w ) = ( F ` v ) ) )
83 40 a1i 
 |-  ( ( F : A -1-1-> B /\ ( w e. A /\ v e. A ) ) -> ( v R w <-> ( F ` v ) S ( F ` w ) ) )
84 80 82 83 3orbi123d 
 |-  ( ( F : A -1-1-> B /\ ( w e. A /\ v e. A ) ) -> ( ( w R v \/ w = v \/ v R w ) <-> ( ( F ` w ) S ( F ` v ) \/ ( F ` w ) = ( F ` v ) \/ ( F ` v ) S ( F ` w ) ) ) )
85 84 2ralbidva 
 |-  ( F : A -1-1-> B -> ( A. w e. A A. v e. A ( w R v \/ w = v \/ v R w ) <-> A. w e. A A. v e. A ( ( F ` w ) S ( F ` v ) \/ ( F ` w ) = ( F ` v ) \/ ( F ` v ) S ( F ` w ) ) ) )
86 breq1 
 |-  ( ( F ` w ) = u -> ( ( F ` w ) S ( F ` v ) <-> u S ( F ` v ) ) )
87 eqeq1 
 |-  ( ( F ` w ) = u -> ( ( F ` w ) = ( F ` v ) <-> u = ( F ` v ) ) )
88 breq2 
 |-  ( ( F ` w ) = u -> ( ( F ` v ) S ( F ` w ) <-> ( F ` v ) S u ) )
89 86 87 88 3orbi123d 
 |-  ( ( F ` w ) = u -> ( ( ( F ` w ) S ( F ` v ) \/ ( F ` w ) = ( F ` v ) \/ ( F ` v ) S ( F ` w ) ) <-> ( u S ( F ` v ) \/ u = ( F ` v ) \/ ( F ` v ) S u ) ) )
90 89 ralbidv 
 |-  ( ( F ` w ) = u -> ( A. v e. A ( ( F ` w ) S ( F ` v ) \/ ( F ` w ) = ( F ` v ) \/ ( F ` v ) S ( F ` w ) ) <-> A. v e. A ( u S ( F ` v ) \/ u = ( F ` v ) \/ ( F ` v ) S u ) ) )
91 90 cbvfo 
 |-  ( F : A -onto-> B -> ( A. w e. A A. v e. A ( ( F ` w ) S ( F ` v ) \/ ( F ` w ) = ( F ` v ) \/ ( F ` v ) S ( F ` w ) ) <-> A. u e. B A. v e. A ( u S ( F ` v ) \/ u = ( F ` v ) \/ ( F ` v ) S u ) ) )
92 breq2 
 |-  ( ( F ` v ) = f -> ( u S ( F ` v ) <-> u S f ) )
93 eqeq2 
 |-  ( ( F ` v ) = f -> ( u = ( F ` v ) <-> u = f ) )
94 breq1 
 |-  ( ( F ` v ) = f -> ( ( F ` v ) S u <-> f S u ) )
95 92 93 94 3orbi123d 
 |-  ( ( F ` v ) = f -> ( ( u S ( F ` v ) \/ u = ( F ` v ) \/ ( F ` v ) S u ) <-> ( u S f \/ u = f \/ f S u ) ) )
96 95 cbvfo 
 |-  ( F : A -onto-> B -> ( A. v e. A ( u S ( F ` v ) \/ u = ( F ` v ) \/ ( F ` v ) S u ) <-> A. f e. B ( u S f \/ u = f \/ f S u ) ) )
97 96 ralbidv 
 |-  ( F : A -onto-> B -> ( A. u e. B A. v e. A ( u S ( F ` v ) \/ u = ( F ` v ) \/ ( F ` v ) S u ) <-> A. u e. B A. f e. B ( u S f \/ u = f \/ f S u ) ) )
98 91 97 bitrd 
 |-  ( F : A -onto-> B -> ( A. w e. A A. v e. A ( ( F ` w ) S ( F ` v ) \/ ( F ` w ) = ( F ` v ) \/ ( F ` v ) S ( F ` w ) ) <-> A. u e. B A. f e. B ( u S f \/ u = f \/ f S u ) ) )
99 85 98 sylan9bb 
 |-  ( ( F : A -1-1-> B /\ F : A -onto-> B ) -> ( A. w e. A A. v e. A ( w R v \/ w = v \/ v R w ) <-> A. u e. B A. f e. B ( u S f \/ u = f \/ f S u ) ) )
100 74 99 sylbi 
 |-  ( F : A -1-1-onto-> B -> ( A. w e. A A. v e. A ( w R v \/ w = v \/ v R w ) <-> A. u e. B A. f e. B ( u S f \/ u = f \/ f S u ) ) )
101 100 biimprd 
 |-  ( F : A -1-1-onto-> B -> ( A. u e. B A. f e. B ( u S f \/ u = f \/ f S u ) -> A. w e. A A. v e. A ( w R v \/ w = v \/ v R w ) ) )
102 73 101 anim12d 
 |-  ( F : A -1-1-onto-> B -> ( ( S Fr B /\ A. u e. B A. f e. B ( u S f \/ u = f \/ f S u ) ) -> ( R Fr A /\ A. w e. A A. v e. A ( w R v \/ w = v \/ v R w ) ) ) )
103 dfwe2 
 |-  ( S We B <-> ( S Fr B /\ A. u e. B A. f e. B ( u S f \/ u = f \/ f S u ) ) )
104 dfwe2 
 |-  ( R We A <-> ( R Fr A /\ A. w e. A A. v e. A ( w R v \/ w = v \/ v R w ) ) )
105 102 103 104 3imtr4g 
 |-  ( F : A -1-1-onto-> B -> ( S We B -> R We A ) )