Metamath Proof Explorer

Theorem fnwe2lem3

Description: Lemma for fnwe2 . Trichotomy. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su 
|- ( z = ( F ` x ) -> S = U )
fnwe2.t 
|- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
fnwe2.s 
|- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
fnwe2.f 
|- ( ph -> ( F |` A ) : A --> B )
fnwe2.r 
|- ( ph -> R We B )
fnwe2lem3.a 
|- ( ph -> a e. A )
fnwe2lem3.b 
|- ( ph -> b e. A )
Assertion fnwe2lem3 
|- ( ph -> ( a T b \/ a = b \/ b T a ) )

Proof

Step Hyp Ref Expression
1 fnwe2.su 
 |-  ( z = ( F ` x ) -> S = U )
2 fnwe2.t 
 |-  T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
3 fnwe2.s 
 |-  ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
4 fnwe2.f 
 |-  ( ph -> ( F |` A ) : A --> B )
5 fnwe2.r 
 |-  ( ph -> R We B )
6 fnwe2lem3.a 
 |-  ( ph -> a e. A )
7 fnwe2lem3.b 
 |-  ( ph -> b e. A )
8 animorrl 
 |-  ( ( ph /\ ( F ` a ) R ( F ` b ) ) -> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )
9 1 2 fnwe2val 
 |-  ( a T b <-> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )
10 8 9 sylibr 
 |-  ( ( ph /\ ( F ` a ) R ( F ` b ) ) -> a T b )
11 10 3mix1d 
 |-  ( ( ph /\ ( F ` a ) R ( F ` b ) ) -> ( a T b \/ a = b \/ b T a ) )
12 simplr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ a [_ ( F ` a ) / z ]_ S b ) -> ( F ` a ) = ( F ` b ) )
13 simpr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ a [_ ( F ` a ) / z ]_ S b ) -> a [_ ( F ` a ) / z ]_ S b )
14 12 13 jca 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ a [_ ( F ` a ) / z ]_ S b ) -> ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) )
15 14 olcd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ a [_ ( F ` a ) / z ]_ S b ) -> ( ( F ` a ) R ( F ` b ) \/ ( ( F ` a ) = ( F ` b ) /\ a [_ ( F ` a ) / z ]_ S b ) ) )
16 15 9 sylibr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ a [_ ( F ` a ) / z ]_ S b ) -> a T b )
17 16 3mix1d 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ a [_ ( F ` a ) / z ]_ S b ) -> ( a T b \/ a = b \/ b T a ) )
18 3mix2 
 |-  ( a = b -> ( a T b \/ a = b \/ b T a ) )
19 18 adantl 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ a = b ) -> ( a T b \/ a = b \/ b T a ) )
20 simplr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ b [_ ( F ` a ) / z ]_ S a ) -> ( F ` a ) = ( F ` b ) )
21 20 eqcomd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ b [_ ( F ` a ) / z ]_ S a ) -> ( F ` b ) = ( F ` a ) )
22 csbeq1 
 |-  ( ( F ` a ) = ( F ` b ) -> [_ ( F ` a ) / z ]_ S = [_ ( F ` b ) / z ]_ S )
23 22 adantl 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> [_ ( F ` a ) / z ]_ S = [_ ( F ` b ) / z ]_ S )
24 23 breqd 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> ( b [_ ( F ` a ) / z ]_ S a <-> b [_ ( F ` b ) / z ]_ S a ) )
25 24 biimpa 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ b [_ ( F ` a ) / z ]_ S a ) -> b [_ ( F ` b ) / z ]_ S a )
26 21 25 jca 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ b [_ ( F ` a ) / z ]_ S a ) -> ( ( F ` b ) = ( F ` a ) /\ b [_ ( F ` b ) / z ]_ S a ) )
27 26 olcd 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ b [_ ( F ` a ) / z ]_ S a ) -> ( ( F ` b ) R ( F ` a ) \/ ( ( F ` b ) = ( F ` a ) /\ b [_ ( F ` b ) / z ]_ S a ) ) )
28 1 2 fnwe2val 
 |-  ( b T a <-> ( ( F ` b ) R ( F ` a ) \/ ( ( F ` b ) = ( F ` a ) /\ b [_ ( F ` b ) / z ]_ S a ) ) )
29 27 28 sylibr 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ b [_ ( F ` a ) / z ]_ S a ) -> b T a )
30 29 3mix3d 
 |-  ( ( ( ph /\ ( F ` a ) = ( F ` b ) ) /\ b [_ ( F ` a ) / z ]_ S a ) -> ( a T b \/ a = b \/ b T a ) )
31 1 2 3 fnwe2lem1 
 |-  ( ( ph /\ a e. A ) -> [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } )
32 6 31 mpdan 
 |-  ( ph -> [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } )
33 weso 
 |-  ( [_ ( F ` a ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` a ) } -> [_ ( F ` a ) / z ]_ S Or { y e. A | ( F ` y ) = ( F ` a ) } )
34 32 33 syl 
 |-  ( ph -> [_ ( F ` a ) / z ]_ S Or { y e. A | ( F ` y ) = ( F ` a ) } )
35 34 adantr 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> [_ ( F ` a ) / z ]_ S Or { y e. A | ( F ` y ) = ( F ` a ) } )
36 fveqeq2 
 |-  ( y = a -> ( ( F ` y ) = ( F ` a ) <-> ( F ` a ) = ( F ` a ) ) )
37 6 adantr 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> a e. A )
38 eqidd 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> ( F ` a ) = ( F ` a ) )
39 36 37 38 elrabd 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> a e. { y e. A | ( F ` y ) = ( F ` a ) } )
40 fveqeq2 
 |-  ( y = b -> ( ( F ` y ) = ( F ` a ) <-> ( F ` b ) = ( F ` a ) ) )
41 7 adantr 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> b e. A )
42 simpr 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> ( F ` a ) = ( F ` b ) )
43 42 eqcomd 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> ( F ` b ) = ( F ` a ) )
44 40 41 43 elrabd 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> b e. { y e. A | ( F ` y ) = ( F ` a ) } )
45 solin 
 |-  ( ( [_ ( F ` a ) / z ]_ S Or { y e. A | ( F ` y ) = ( F ` a ) } /\ ( a e. { y e. A | ( F ` y ) = ( F ` a ) } /\ b e. { y e. A | ( F ` y ) = ( F ` a ) } ) ) -> ( a [_ ( F ` a ) / z ]_ S b \/ a = b \/ b [_ ( F ` a ) / z ]_ S a ) )
46 35 39 44 45 syl12anc 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> ( a [_ ( F ` a ) / z ]_ S b \/ a = b \/ b [_ ( F ` a ) / z ]_ S a ) )
47 17 19 30 46 mpjao3dan 
 |-  ( ( ph /\ ( F ` a ) = ( F ` b ) ) -> ( a T b \/ a = b \/ b T a ) )
48 animorrl 
 |-  ( ( ph /\ ( F ` b ) R ( F ` a ) ) -> ( ( F ` b ) R ( F ` a ) \/ ( ( F ` b ) = ( F ` a ) /\ b [_ ( F ` b ) / z ]_ S a ) ) )
49 48 28 sylibr 
 |-  ( ( ph /\ ( F ` b ) R ( F ` a ) ) -> b T a )
50 49 3mix3d 
 |-  ( ( ph /\ ( F ` b ) R ( F ` a ) ) -> ( a T b \/ a = b \/ b T a ) )
51 weso 
 |-  ( R We B -> R Or B )
52 5 51 syl 
 |-  ( ph -> R Or B )
53 6 fvresd 
 |-  ( ph -> ( ( F |` A ) ` a ) = ( F ` a ) )
54 4 6 ffvelrnd 
 |-  ( ph -> ( ( F |` A ) ` a ) e. B )
55 53 54 eqeltrrd 
 |-  ( ph -> ( F ` a ) e. B )
56 7 fvresd 
 |-  ( ph -> ( ( F |` A ) ` b ) = ( F ` b ) )
57 4 7 ffvelrnd 
 |-  ( ph -> ( ( F |` A ) ` b ) e. B )
58 56 57 eqeltrrd 
 |-  ( ph -> ( F ` b ) e. B )
59 solin 
 |-  ( ( R Or B /\ ( ( F ` a ) e. B /\ ( F ` b ) e. B ) ) -> ( ( F ` a ) R ( F ` b ) \/ ( F ` a ) = ( F ` b ) \/ ( F ` b ) R ( F ` a ) ) )
60 52 55 58 59 syl12anc 
 |-  ( ph -> ( ( F ` a ) R ( F ` b ) \/ ( F ` a ) = ( F ` b ) \/ ( F ` b ) R ( F ` a ) ) )
61 11 47 50 60 mpjao3dan 
 |-  ( ph -> ( a T b \/ a = b \/ b T a ) )