Metamath Proof Explorer

Theorem fnwe2lem4

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 𝐵 )
fnwe2lem4.a ⊢ ( 𝜑 → 𝑎 ∈ 𝐴 )
fnwe2lem4.b ⊢ ( 𝜑 → 𝑏 ∈ 𝐴 )
Assertion fnwe2lem4 ( 𝜑 → ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) )

Proof

Step Hyp Ref Expression
1 fnwe2.su ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
2 fnwe2.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
3 fnwe2.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
4 fnwe2.f ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) : 𝐴 ⟶ 𝐵 )
5 fnwe2.r ⊢ ( 𝜑 → 𝑅 We 𝐵 )
6 fnwe2lem4.a ⊢ ( 𝜑 → 𝑎 ∈ 𝐴 )
7 fnwe2lem4.b ⊢ ( 𝜑 → 𝑏 ∈ 𝐴 )
8 animorrl ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )
9 1 2 fnwe2lem1 ⊢ ( 𝑎 𝑇 𝑏 ↔ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )
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 fnwe2lem1 ⊢ ( 𝑏 𝑇 𝑎 ↔ ( ( 𝐹 ‘ 𝑏 ) 𝑅 ( 𝐹 ‘ 𝑎 ) ∨ ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ∧ 𝑏 ⦋ ( 𝐹 ‘ 𝑏 ) / 𝑧 ⦌ 𝑆 𝑎 ) ) )
29 27 28 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ 𝑏 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑎 ) → 𝑏 𝑇 𝑎 )
30 29 3mix3d ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) ∧ 𝑏 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑎 ) → ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) )
31 1 2 3 fnwe2lem2 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 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 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑎 ) ∈ 𝐵 )
55 53 54 eqeltrrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 )
56 7 fvresd ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) = ( 𝐹 ‘ 𝑏 ) )
57 4 7 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑏 ) ∈ 𝐵 )
58 56 57 eqeltrrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑏 ) ∈ 𝐵 )
59 solin ⊢ ( ( 𝑅 Or 𝐵 ∧ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑏 ) ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∨ ( 𝐹 ‘ 𝑏 ) 𝑅 ( 𝐹 ‘ 𝑎 ) ) )
60 52 55 58 59 syl12anc ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∨ ( 𝐹 ‘ 𝑏 ) 𝑅 ( 𝐹 ‘ 𝑎 ) ) )
61 11 47 50 60 mpjao3dan ⊢ ( 𝜑 → ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) )