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 |
⊢ ( 𝜑 → ( 𝑎 𝑇 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑇 𝑎 ) ) |