Metamath Proof Explorer


Theorem fnwe2lem3

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

Ref Expression
Hypotheses fnwe2.su z=FxS=U
fnwe2.t T=xy|FxRFyFx=FyxUy
fnwe2.s φxAUWeyA|Fy=Fx
fnwe2.f φFA:AB
fnwe2.r φRWeB
fnwe2lem3.a φaA
fnwe2lem3.b φbA
Assertion fnwe2lem3 φaTba=bbTa

Proof

Step Hyp Ref Expression
1 fnwe2.su z=FxS=U
2 fnwe2.t T=xy|FxRFyFx=FyxUy
3 fnwe2.s φxAUWeyA|Fy=Fx
4 fnwe2.f φFA:AB
5 fnwe2.r φRWeB
6 fnwe2lem3.a φaA
7 fnwe2lem3.b φbA
8 animorrl φFaRFbFaRFbFa=FbaFa/zSb
9 1 2 fnwe2val aTbFaRFbFa=FbaFa/zSb
10 8 9 sylibr φFaRFbaTb
11 10 3mix1d φFaRFbaTba=bbTa
12 simplr φFa=FbaFa/zSbFa=Fb
13 simpr φFa=FbaFa/zSbaFa/zSb
14 12 13 jca φFa=FbaFa/zSbFa=FbaFa/zSb
15 14 olcd φFa=FbaFa/zSbFaRFbFa=FbaFa/zSb
16 15 9 sylibr φFa=FbaFa/zSbaTb
17 16 3mix1d φFa=FbaFa/zSbaTba=bbTa
18 3mix2 a=baTba=bbTa
19 18 adantl φFa=Fba=baTba=bbTa
20 simplr φFa=FbbFa/zSaFa=Fb
21 20 eqcomd φFa=FbbFa/zSaFb=Fa
22 csbeq1 Fa=FbFa/zS=Fb/zS
23 22 adantl φFa=FbFa/zS=Fb/zS
24 23 breqd φFa=FbbFa/zSabFb/zSa
25 24 biimpa φFa=FbbFa/zSabFb/zSa
26 21 25 jca φFa=FbbFa/zSaFb=FabFb/zSa
27 26 olcd φFa=FbbFa/zSaFbRFaFb=FabFb/zSa
28 1 2 fnwe2val bTaFbRFaFb=FabFb/zSa
29 27 28 sylibr φFa=FbbFa/zSabTa
30 29 3mix3d φFa=FbbFa/zSaaTba=bbTa
31 1 2 3 fnwe2lem1 φaAFa/zSWeyA|Fy=Fa
32 6 31 mpdan φFa/zSWeyA|Fy=Fa
33 weso Fa/zSWeyA|Fy=FaFa/zSOryA|Fy=Fa
34 32 33 syl φFa/zSOryA|Fy=Fa
35 34 adantr φFa=FbFa/zSOryA|Fy=Fa
36 fveqeq2 y=aFy=FaFa=Fa
37 6 adantr φFa=FbaA
38 eqidd φFa=FbFa=Fa
39 36 37 38 elrabd φFa=FbayA|Fy=Fa
40 fveqeq2 y=bFy=FaFb=Fa
41 7 adantr φFa=FbbA
42 simpr φFa=FbFa=Fb
43 42 eqcomd φFa=FbFb=Fa
44 40 41 43 elrabd φFa=FbbyA|Fy=Fa
45 solin Fa/zSOryA|Fy=FaayA|Fy=FabyA|Fy=FaaFa/zSba=bbFa/zSa
46 35 39 44 45 syl12anc φFa=FbaFa/zSba=bbFa/zSa
47 17 19 30 46 mpjao3dan φFa=FbaTba=bbTa
48 animorrl φFbRFaFbRFaFb=FabFb/zSa
49 48 28 sylibr φFbRFabTa
50 49 3mix3d φFbRFaaTba=bbTa
51 weso RWeBROrB
52 5 51 syl φROrB
53 6 fvresd φFAa=Fa
54 4 6 ffvelrnd φFAaB
55 53 54 eqeltrrd φFaB
56 7 fvresd φFAb=Fb
57 4 7 ffvelrnd φFAbB
58 56 57 eqeltrrd φFbB
59 solin ROrBFaBFbBFaRFbFa=FbFbRFa
60 52 55 58 59 syl12anc φFaRFbFa=FbFbRFa
61 11 47 50 60 mpjao3dan φaTba=bbTa