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 φ x A U We y A | F y = F x
fnwe2.f φ F A : A B
fnwe2.r φ R We B
fnwe2lem3.a φ a A
fnwe2lem3.b φ b A
Assertion fnwe2lem3 φ 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 φ x A U We y A | F y = F x
4 fnwe2.f φ F A : A B
5 fnwe2.r φ R We B
6 fnwe2lem3.a φ a A
7 fnwe2lem3.b φ b A
8 animorrl φ 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 φ F a R F b a T b
11 10 3mix1d φ F a R F b a T b a = b b T a
12 simplr φ F a = F b a F a / z S b F a = F b
13 simpr φ F a = F b a F a / z S b a F a / z S b
14 12 13 jca φ F a = F b a F a / z S b F a = F b a F a / z S b
15 14 olcd φ 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 φ F a = F b a F a / z S b a T b
17 16 3mix1d φ 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 φ F a = F b a = b a T b a = b b T a
20 simplr φ F a = F b b F a / z S a F a = F b
21 20 eqcomd φ 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 φ F a = F b F a / z S = F b / z S
24 23 breqd φ F a = F b b F a / z S a b F b / z S a
25 24 biimpa φ F a = F b b F a / z S a b F b / z S a
26 21 25 jca φ F a = F b b F a / z S a F b = F a b F b / z S a
27 26 olcd φ 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 φ F a = F b b F a / z S a b T a
30 29 3mix3d φ F a = F b b F a / z S a a T b a = b b T a
31 1 2 3 fnwe2lem1 φ a A F a / z S We y A | F y = F a
32 6 31 mpdan φ F a / z S We y A | F y = F a
33 weso F a / z S We y A | F y = F a F a / z S Or y A | F y = F a
34 32 33 syl φ F a / z S Or y A | F y = F a
35 34 adantr φ F a = F b F a / z S Or y A | F y = F a
36 fveqeq2 y = a F y = F a F a = F a
37 6 adantr φ F a = F b a A
38 eqidd φ F a = F b F a = F a
39 36 37 38 elrabd φ F a = F b a y A | F y = F a
40 fveqeq2 y = b F y = F a F b = F a
41 7 adantr φ F a = F b b A
42 simpr φ F a = F b F a = F b
43 42 eqcomd φ F a = F b F b = F a
44 40 41 43 elrabd φ F a = F b b y A | F y = F a
45 solin F a / z S Or y A | F y = F a a y A | F y = F a b y 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 φ F a = F b a F a / z S b a = b b F a / z S a
47 17 19 30 46 mpjao3dan φ F a = F b a T b a = b b T a
48 animorrl φ F b R F a F b R F a F b = F a b F b / z S a
49 48 28 sylibr φ F b R F a b T a
50 49 3mix3d φ 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 φ R Or B
53 6 fvresd φ F A a = F a
54 4 6 ffvelrnd φ F A a B
55 53 54 eqeltrrd φ F a B
56 7 fvresd φ F A b = F b
57 4 7 ffvelrnd φ F A b B
58 56 57 eqeltrrd φ F b B
59 solin R Or B F a B F b B F a R F b F a = F b F b R F a
60 52 55 58 59 syl12anc φ F a R F b F a = F b F b R F a
61 11 47 50 60 mpjao3dan φ a T b a = b b T a