Metamath Proof Explorer

Theorem imasleval

Description: The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses imasless.u 
|- ( ph -> U = ( F "s R ) )
imasless.v 
|- ( ph -> V = ( Base ` R ) )
imasless.f 
|- ( ph -> F : V -onto-> B )
imasless.r 
|- ( ph -> R e. Z )
imasless.l 
|- .<_ = ( le ` U )
imasleval.n 
|- N = ( le ` R )
imasleval.e 
|- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( c e. V /\ d e. V ) ) -> ( ( ( F ` a ) = ( F ` c ) /\ ( F ` b ) = ( F ` d ) ) -> ( a N b <-> c N d ) ) )
Assertion imasleval 
|- ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .<_ ( F ` Y ) <-> X N Y ) )

Proof

Step Hyp Ref Expression
1 imasless.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasless.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasless.f 
 |-  ( ph -> F : V -onto-> B )
4 imasless.r 
 |-  ( ph -> R e. Z )
5 imasless.l 
 |-  .<_ = ( le ` U )
6 imasleval.n 
 |-  N = ( le ` R )
7 imasleval.e 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( c e. V /\ d e. V ) ) -> ( ( ( F ` a ) = ( F ` c ) /\ ( F ` b ) = ( F ` d ) ) -> ( a N b <-> c N d ) ) )
8 fveq2 
 |-  ( c = X -> ( F ` c ) = ( F ` X ) )
9 8 breq1d 
 |-  ( c = X -> ( ( F ` c ) .<_ ( F ` d ) <-> ( F ` X ) .<_ ( F ` d ) ) )
10 breq1 
 |-  ( c = X -> ( c N d <-> X N d ) )
11 9 10 bibi12d 
 |-  ( c = X -> ( ( ( F ` c ) .<_ ( F ` d ) <-> c N d ) <-> ( ( F ` X ) .<_ ( F ` d ) <-> X N d ) ) )
12 11 imbi2d 
 |-  ( c = X -> ( ( ph -> ( ( F ` c ) .<_ ( F ` d ) <-> c N d ) ) <-> ( ph -> ( ( F ` X ) .<_ ( F ` d ) <-> X N d ) ) ) )
13 fveq2 
 |-  ( d = Y -> ( F ` d ) = ( F ` Y ) )
14 13 breq2d 
 |-  ( d = Y -> ( ( F ` X ) .<_ ( F ` d ) <-> ( F ` X ) .<_ ( F ` Y ) ) )
15 breq2 
 |-  ( d = Y -> ( X N d <-> X N Y ) )
16 14 15 bibi12d 
 |-  ( d = Y -> ( ( ( F ` X ) .<_ ( F ` d ) <-> X N d ) <-> ( ( F ` X ) .<_ ( F ` Y ) <-> X N Y ) ) )
17 16 imbi2d 
 |-  ( d = Y -> ( ( ph -> ( ( F ` X ) .<_ ( F ` d ) <-> X N d ) ) <-> ( ph -> ( ( F ` X ) .<_ ( F ` Y ) <-> X N Y ) ) ) )
18 fofn 
 |-  ( F : V -onto-> B -> F Fn V )
19 3 18 syl 
 |-  ( ph -> F Fn V )
20 19 adantr 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> F Fn V )
21 20 fndmd 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> dom F = V )
22 21 rexeqdv 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( E. a e. dom F ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> E. a e. V ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) ) )
23 fnbrfvb 
 |-  ( ( F Fn V /\ a e. V ) -> ( ( F ` a ) = ( F ` c ) <-> a F ( F ` c ) ) )
24 20 23 sylan 
 |-  ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) -> ( ( F ` a ) = ( F ` c ) <-> a F ( F ` c ) ) )
25 24 anbi1d 
 |-  ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) -> ( ( ( F ` a ) = ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) ) )
26 ancom 
 |-  ( ( a N b /\ b F ( F ` d ) ) <-> ( b F ( F ` d ) /\ a N b ) )
27 vex 
 |-  b e. _V
28 fvex 
 |-  ( F ` d ) e. _V
29 27 28 breldm 
 |-  ( b F ( F ` d ) -> b e. dom F )
30 29 adantr 
 |-  ( ( b F ( F ` d ) /\ a N b ) -> b e. dom F )
31 30 pm4.71ri 
 |-  ( ( b F ( F ` d ) /\ a N b ) <-> ( b e. dom F /\ ( b F ( F ` d ) /\ a N b ) ) )
32 26 31 bitri 
 |-  ( ( a N b /\ b F ( F ` d ) ) <-> ( b e. dom F /\ ( b F ( F ` d ) /\ a N b ) ) )
33 32 exbii 
 |-  ( E. b ( a N b /\ b F ( F ` d ) ) <-> E. b ( b e. dom F /\ ( b F ( F ` d ) /\ a N b ) ) )
34 vex 
 |-  a e. _V
35 34 28 brco 
 |-  ( a ( F o. N ) ( F ` d ) <-> E. b ( a N b /\ b F ( F ` d ) ) )
36 df-rex 
 |-  ( E. b e. dom F ( b F ( F ` d ) /\ a N b ) <-> E. b ( b e. dom F /\ ( b F ( F ` d ) /\ a N b ) ) )
37 33 35 36 3bitr4i 
 |-  ( a ( F o. N ) ( F ` d ) <-> E. b e. dom F ( b F ( F ` d ) /\ a N b ) )
38 20 ad2antrr 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) -> F Fn V )
39 fnbrfvb 
 |-  ( ( F Fn V /\ b e. V ) -> ( ( F ` b ) = ( F ` d ) <-> b F ( F ` d ) ) )
40 38 39 sylan 
 |-  ( ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) /\ b e. V ) -> ( ( F ` b ) = ( F ` d ) <-> b F ( F ` d ) ) )
41 40 anbi1d 
 |-  ( ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) /\ b e. V ) -> ( ( ( F ` b ) = ( F ` d ) /\ a N b ) <-> ( b F ( F ` d ) /\ a N b ) ) )
42 7 3expa 
 |-  ( ( ( ph /\ ( a e. V /\ b e. V ) ) /\ ( c e. V /\ d e. V ) ) -> ( ( ( F ` a ) = ( F ` c ) /\ ( F ` b ) = ( F ` d ) ) -> ( a N b <-> c N d ) ) )
43 42 an32s 
 |-  ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ ( a e. V /\ b e. V ) ) -> ( ( ( F ` a ) = ( F ` c ) /\ ( F ` b ) = ( F ` d ) ) -> ( a N b <-> c N d ) ) )
44 43 anassrs 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ b e. V ) -> ( ( ( F ` a ) = ( F ` c ) /\ ( F ` b ) = ( F ` d ) ) -> ( a N b <-> c N d ) ) )
45 44 impl 
 |-  ( ( ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ b e. V ) /\ ( F ` a ) = ( F ` c ) ) /\ ( F ` b ) = ( F ` d ) ) -> ( a N b <-> c N d ) )
46 45 pm5.32da 
 |-  ( ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ b e. V ) /\ ( F ` a ) = ( F ` c ) ) -> ( ( ( F ` b ) = ( F ` d ) /\ a N b ) <-> ( ( F ` b ) = ( F ` d ) /\ c N d ) ) )
47 46 an32s 
 |-  ( ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) /\ b e. V ) -> ( ( ( F ` b ) = ( F ` d ) /\ a N b ) <-> ( ( F ` b ) = ( F ` d ) /\ c N d ) ) )
48 41 47 bitr3d 
 |-  ( ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) /\ b e. V ) -> ( ( b F ( F ` d ) /\ a N b ) <-> ( ( F ` b ) = ( F ` d ) /\ c N d ) ) )
49 48 rexbidva 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) -> ( E. b e. V ( b F ( F ` d ) /\ a N b ) <-> E. b e. V ( ( F ` b ) = ( F ` d ) /\ c N d ) ) )
50 r19.41v 
 |-  ( E. b e. V ( ( F ` b ) = ( F ` d ) /\ c N d ) <-> ( E. b e. V ( F ` b ) = ( F ` d ) /\ c N d ) )
51 49 50 bitrdi 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) -> ( E. b e. V ( b F ( F ` d ) /\ a N b ) <-> ( E. b e. V ( F ` b ) = ( F ` d ) /\ c N d ) ) )
52 21 rexeqdv 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( E. b e. dom F ( b F ( F ` d ) /\ a N b ) <-> E. b e. V ( b F ( F ` d ) /\ a N b ) ) )
53 52 ad2antrr 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) -> ( E. b e. dom F ( b F ( F ` d ) /\ a N b ) <-> E. b e. V ( b F ( F ` d ) /\ a N b ) ) )
54 simprr 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> d e. V )
55 eqid 
 |-  ( F ` d ) = ( F ` d )
56 fveqeq2 
 |-  ( b = d -> ( ( F ` b ) = ( F ` d ) <-> ( F ` d ) = ( F ` d ) ) )
57 56 rspcev 
 |-  ( ( d e. V /\ ( F ` d ) = ( F ` d ) ) -> E. b e. V ( F ` b ) = ( F ` d ) )
58 54 55 57 sylancl 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> E. b e. V ( F ` b ) = ( F ` d ) )
59 58 biantrurd 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( c N d <-> ( E. b e. V ( F ` b ) = ( F ` d ) /\ c N d ) ) )
60 59 ad2antrr 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) -> ( c N d <-> ( E. b e. V ( F ` b ) = ( F ` d ) /\ c N d ) ) )
61 51 53 60 3bitr4d 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) -> ( E. b e. dom F ( b F ( F ` d ) /\ a N b ) <-> c N d ) )
62 37 61 bitrid 
 |-  ( ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) /\ ( F ` a ) = ( F ` c ) ) -> ( a ( F o. N ) ( F ` d ) <-> c N d ) )
63 62 pm5.32da 
 |-  ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) -> ( ( ( F ` a ) = ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> ( ( F ` a ) = ( F ` c ) /\ c N d ) ) )
64 25 63 bitr3d 
 |-  ( ( ( ph /\ ( c e. V /\ d e. V ) ) /\ a e. V ) -> ( ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> ( ( F ` a ) = ( F ` c ) /\ c N d ) ) )
65 64 rexbidva 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( E. a e. V ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> E. a e. V ( ( F ` a ) = ( F ` c ) /\ c N d ) ) )
66 22 65 bitrd 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( E. a e. dom F ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> E. a e. V ( ( F ` a ) = ( F ` c ) /\ c N d ) ) )
67 fvex 
 |-  ( F ` c ) e. _V
68 67 34 brcnv 
 |-  ( ( F ` c ) `' F a <-> a F ( F ` c ) )
69 68 anbi1i 
 |-  ( ( ( F ` c ) `' F a /\ a ( F o. N ) ( F ` d ) ) <-> ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) )
70 34 67 breldm 
 |-  ( a F ( F ` c ) -> a e. dom F )
71 70 adantr 
 |-  ( ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) -> a e. dom F )
72 71 pm4.71ri 
 |-  ( ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> ( a e. dom F /\ ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) ) )
73 69 72 bitri 
 |-  ( ( ( F ` c ) `' F a /\ a ( F o. N ) ( F ` d ) ) <-> ( a e. dom F /\ ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) ) )
74 73 exbii 
 |-  ( E. a ( ( F ` c ) `' F a /\ a ( F o. N ) ( F ` d ) ) <-> E. a ( a e. dom F /\ ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) ) )
75 67 28 brco 
 |-  ( ( F ` c ) ( ( F o. N ) o. `' F ) ( F ` d ) <-> E. a ( ( F ` c ) `' F a /\ a ( F o. N ) ( F ` d ) ) )
76 df-rex 
 |-  ( E. a e. dom F ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> E. a ( a e. dom F /\ ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) ) )
77 74 75 76 3bitr4ri 
 |-  ( E. a e. dom F ( a F ( F ` c ) /\ a ( F o. N ) ( F ` d ) ) <-> ( F ` c ) ( ( F o. N ) o. `' F ) ( F ` d ) )
78 r19.41v 
 |-  ( E. a e. V ( ( F ` a ) = ( F ` c ) /\ c N d ) <-> ( E. a e. V ( F ` a ) = ( F ` c ) /\ c N d ) )
79 66 77 78 3bitr3g 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( ( F ` c ) ( ( F o. N ) o. `' F ) ( F ` d ) <-> ( E. a e. V ( F ` a ) = ( F ` c ) /\ c N d ) ) )
80 1 2 3 4 6 5 imasle 
 |-  ( ph -> .<_ = ( ( F o. N ) o. `' F ) )
81 80 adantr 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> .<_ = ( ( F o. N ) o. `' F ) )
82 81 breqd 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( ( F ` c ) .<_ ( F ` d ) <-> ( F ` c ) ( ( F o. N ) o. `' F ) ( F ` d ) ) )
83 simprl 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> c e. V )
84 eqid 
 |-  ( F ` c ) = ( F ` c )
85 fveqeq2 
 |-  ( a = c -> ( ( F ` a ) = ( F ` c ) <-> ( F ` c ) = ( F ` c ) ) )
86 85 rspcev 
 |-  ( ( c e. V /\ ( F ` c ) = ( F ` c ) ) -> E. a e. V ( F ` a ) = ( F ` c ) )
87 83 84 86 sylancl 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> E. a e. V ( F ` a ) = ( F ` c ) )
88 87 biantrurd 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( c N d <-> ( E. a e. V ( F ` a ) = ( F ` c ) /\ c N d ) ) )
89 79 82 88 3bitr4d 
 |-  ( ( ph /\ ( c e. V /\ d e. V ) ) -> ( ( F ` c ) .<_ ( F ` d ) <-> c N d ) )
90 89 expcom 
 |-  ( ( c e. V /\ d e. V ) -> ( ph -> ( ( F ` c ) .<_ ( F ` d ) <-> c N d ) ) )
91 12 17 90 vtocl2ga 
 |-  ( ( X e. V /\ Y e. V ) -> ( ph -> ( ( F ` X ) .<_ ( F ` Y ) <-> X N Y ) ) )
92 91 com12 
 |-  ( ph -> ( ( X e. V /\ Y e. V ) -> ( ( F ` X ) .<_ ( F ` Y ) <-> X N Y ) ) )
93 92 3impib 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .<_ ( F ` Y ) <-> X N Y ) )