Metamath Proof Explorer


Theorem fnwe2lem3

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

Ref Expression
Hypotheses fnwe2.su ( 𝑧 = ( 𝐹𝑥 ) → 𝑆 = 𝑈 )
fnwe2.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ∨ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
fnwe2.s ( ( 𝜑𝑥𝐴 ) → 𝑈 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑥 ) } )
fnwe2.f ( 𝜑 → ( 𝐹𝐴 ) : 𝐴𝐵 )
fnwe2.r ( 𝜑𝑅 We 𝐵 )
fnwe2lem3.a ( 𝜑𝑎𝐴 )
fnwe2lem3.b ( 𝜑𝑏𝐴 )
Assertion fnwe2lem3 ( 𝜑 → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )

Proof

Step Hyp Ref Expression
1 fnwe2.su ( 𝑧 = ( 𝐹𝑥 ) → 𝑆 = 𝑈 )
2 fnwe2.t 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹𝑥 ) 𝑅 ( 𝐹𝑦 ) ∨ ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
3 fnwe2.s ( ( 𝜑𝑥𝐴 ) → 𝑈 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑥 ) } )
4 fnwe2.f ( 𝜑 → ( 𝐹𝐴 ) : 𝐴𝐵 )
5 fnwe2.r ( 𝜑𝑅 We 𝐵 )
6 fnwe2lem3.a ( 𝜑𝑎𝐴 )
7 fnwe2lem3.b ( 𝜑𝑏𝐴 )
8 animorrl ( ( 𝜑 ∧ ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ) → ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ∨ ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) ) )
9 1 2 fnwe2val ( 𝑎 𝑇 𝑏 ↔ ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ∨ ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) ) )
10 8 9 sylibr ( ( 𝜑 ∧ ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ) → 𝑎 𝑇 𝑏 )
11 10 3mix1d ( ( 𝜑 ∧ ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ) → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
12 simplr ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) → ( 𝐹𝑎 ) = ( 𝐹𝑏 ) )
13 simpr ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) → 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 )
14 12 13 jca ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) → ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) )
15 14 olcd ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) → ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ∨ ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) ) )
16 15 9 sylibr ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) → 𝑎 𝑇 𝑏 )
17 16 3mix1d ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
18 3mix2 ( 𝑎 = 𝑏 → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
19 18 adantl ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑎 = 𝑏 ) → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
20 simplr ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) → ( 𝐹𝑎 ) = ( 𝐹𝑏 ) )
21 20 eqcomd ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) → ( 𝐹𝑏 ) = ( 𝐹𝑎 ) )
22 csbeq1 ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) → ( 𝐹𝑎 ) / 𝑧 𝑆 = ( 𝐹𝑏 ) / 𝑧 𝑆 )
23 22 adantl ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝐹𝑎 ) / 𝑧 𝑆 = ( 𝐹𝑏 ) / 𝑧 𝑆 )
24 23 breqd ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎𝑏 ( 𝐹𝑏 ) / 𝑧 𝑆 𝑎 ) )
25 24 biimpa ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) → 𝑏 ( 𝐹𝑏 ) / 𝑧 𝑆 𝑎 )
26 21 25 jca ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) → ( ( 𝐹𝑏 ) = ( 𝐹𝑎 ) ∧ 𝑏 ( 𝐹𝑏 ) / 𝑧 𝑆 𝑎 ) )
27 26 olcd ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) → ( ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ∨ ( ( 𝐹𝑏 ) = ( 𝐹𝑎 ) ∧ 𝑏 ( 𝐹𝑏 ) / 𝑧 𝑆 𝑎 ) ) )
28 1 2 fnwe2val ( 𝑏 𝑇 𝑎 ↔ ( ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ∨ ( ( 𝐹𝑏 ) = ( 𝐹𝑎 ) ∧ 𝑏 ( 𝐹𝑏 ) / 𝑧 𝑆 𝑎 ) ) )
29 27 28 sylibr ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) → 𝑏 𝑇 𝑎 )
30 29 3mix3d ( ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) ∧ 𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
31 1 2 3 fnwe2lem1 ( ( 𝜑𝑎𝐴 ) → ( 𝐹𝑎 ) / 𝑧 𝑆 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } )
32 6 31 mpdan ( 𝜑 ( 𝐹𝑎 ) / 𝑧 𝑆 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } )
33 weso ( ( 𝐹𝑎 ) / 𝑧 𝑆 We { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } → ( 𝐹𝑎 ) / 𝑧 𝑆 Or { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } )
34 32 33 syl ( 𝜑 ( 𝐹𝑎 ) / 𝑧 𝑆 Or { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } )
35 34 adantr ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝐹𝑎 ) / 𝑧 𝑆 Or { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } )
36 fveqeq2 ( 𝑦 = 𝑎 → ( ( 𝐹𝑦 ) = ( 𝐹𝑎 ) ↔ ( 𝐹𝑎 ) = ( 𝐹𝑎 ) ) )
37 6 adantr ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → 𝑎𝐴 )
38 eqidd ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝐹𝑎 ) = ( 𝐹𝑎 ) )
39 36 37 38 elrabd ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → 𝑎 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } )
40 fveqeq2 ( 𝑦 = 𝑏 → ( ( 𝐹𝑦 ) = ( 𝐹𝑎 ) ↔ ( 𝐹𝑏 ) = ( 𝐹𝑎 ) ) )
41 7 adantr ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → 𝑏𝐴 )
42 simpr ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝐹𝑎 ) = ( 𝐹𝑏 ) )
43 42 eqcomd ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝐹𝑏 ) = ( 𝐹𝑎 ) )
44 40 41 43 elrabd ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → 𝑏 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } )
45 solin ( ( ( 𝐹𝑎 ) / 𝑧 𝑆 Or { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } ∧ ( 𝑎 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } ∧ 𝑏 ∈ { 𝑦𝐴 ∣ ( 𝐹𝑦 ) = ( 𝐹𝑎 ) } ) ) → ( 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏𝑎 = 𝑏𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) )
46 35 39 44 45 syl12anc ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏𝑎 = 𝑏𝑏 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑎 ) )
47 17 19 30 46 mpjao3dan ( ( 𝜑 ∧ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ) → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
48 animorrl ( ( 𝜑 ∧ ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ) → ( ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ∨ ( ( 𝐹𝑏 ) = ( 𝐹𝑎 ) ∧ 𝑏 ( 𝐹𝑏 ) / 𝑧 𝑆 𝑎 ) ) )
49 48 28 sylibr ( ( 𝜑 ∧ ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ) → 𝑏 𝑇 𝑎 )
50 49 3mix3d ( ( 𝜑 ∧ ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ) → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )
51 weso ( 𝑅 We 𝐵𝑅 Or 𝐵 )
52 5 51 syl ( 𝜑𝑅 Or 𝐵 )
53 6 fvresd ( 𝜑 → ( ( 𝐹𝐴 ) ‘ 𝑎 ) = ( 𝐹𝑎 ) )
54 4 6 ffvelrnd ( 𝜑 → ( ( 𝐹𝐴 ) ‘ 𝑎 ) ∈ 𝐵 )
55 53 54 eqeltrrd ( 𝜑 → ( 𝐹𝑎 ) ∈ 𝐵 )
56 7 fvresd ( 𝜑 → ( ( 𝐹𝐴 ) ‘ 𝑏 ) = ( 𝐹𝑏 ) )
57 4 7 ffvelrnd ( 𝜑 → ( ( 𝐹𝐴 ) ‘ 𝑏 ) ∈ 𝐵 )
58 56 57 eqeltrrd ( 𝜑 → ( 𝐹𝑏 ) ∈ 𝐵 )
59 solin ( ( 𝑅 Or 𝐵 ∧ ( ( 𝐹𝑎 ) ∈ 𝐵 ∧ ( 𝐹𝑏 ) ∈ 𝐵 ) ) → ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ∨ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ∨ ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ) )
60 52 55 58 59 syl12anc ( 𝜑 → ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ∨ ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ∨ ( 𝐹𝑏 ) 𝑅 ( 𝐹𝑎 ) ) )
61 11 47 50 60 mpjao3dan ( 𝜑 → ( 𝑎 𝑇 𝑏𝑎 = 𝑏𝑏 𝑇 𝑎 ) )