Proof of Theorem fnwe2lem3
Step | Hyp | Ref
| Expression |
1 | | orc 894 |
. . . . 5
⊢ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
2 | 1 | adantl 474 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
3 | | fnwe2.su |
. . . . 5
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) |
4 | | fnwe2.t |
. . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} |
5 | 3, 4 | fnwe2val 38404 |
. . . 4
⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
6 | 2, 5 | sylibr 226 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → 𝑎𝑇𝑏) |
7 | 6 | 3mix1d 1436 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
8 | | simplr 786 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝐹‘𝑎) = (𝐹‘𝑏)) |
9 | | simpr 478 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) |
10 | 8, 9 | jca 508 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)) |
11 | 10 | olcd 901 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
12 | 11, 5 | sylibr 226 |
. . . 4
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎𝑇𝑏) |
13 | 12 | 3mix1d 1436 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
14 | | 3mix2 1431 |
. . . 4
⊢ (𝑎 = 𝑏 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
15 | 14 | adantl 474 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎 = 𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
16 | | simplr 786 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑎) = (𝐹‘𝑏)) |
17 | 16 | eqcomd 2805 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑏) = (𝐹‘𝑎)) |
18 | | csbeq1 3731 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑎) = (𝐹‘𝑏) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆) |
19 | 18 | adantl 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆) |
20 | 19 | breqd 4854 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎 ↔ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)) |
21 | 20 | biimpa 469 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎) |
22 | 17, 21 | jca 508 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)) |
23 | 22 | olcd 901 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
24 | 3, 4 | fnwe2val 38404 |
. . . . 5
⊢ (𝑏𝑇𝑎 ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
25 | 23, 24 | sylibr 226 |
. . . 4
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏𝑇𝑎) |
26 | 25 | 3mix3d 1438 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
27 | | fnwe2lem3.a |
. . . . . . 7
⊢ (𝜑 → 𝑎 ∈ 𝐴) |
28 | | fnwe2.s |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) |
29 | 3, 4, 28 | fnwe2lem1 38405 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
30 | 27, 29 | mpdan 679 |
. . . . . 6
⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
31 | | weso 5303 |
. . . . . 6
⊢
(⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
33 | 32 | adantr 473 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
34 | 27 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ 𝐴) |
35 | | eqidd 2800 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑎)) |
36 | | fveqeq2 6420 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑎) = (𝐹‘𝑎))) |
37 | 36 | elrab 3556 |
. . . . 5
⊢ (𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ↔ (𝑎 ∈ 𝐴 ∧ (𝐹‘𝑎) = (𝐹‘𝑎))) |
38 | 34, 35, 37 | sylanbrc 579 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
39 | | fnwe2lem3.b |
. . . . . 6
⊢ (𝜑 → 𝑏 ∈ 𝐴) |
40 | 39 | adantr 473 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ 𝐴) |
41 | | simpr 478 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑏)) |
42 | 41 | eqcomd 2805 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑏) = (𝐹‘𝑎)) |
43 | | fveqeq2 6420 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑏) = (𝐹‘𝑎))) |
44 | 43 | elrab 3556 |
. . . . 5
⊢ (𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ↔ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑏) = (𝐹‘𝑎))) |
45 | 40, 42, 44 | sylanbrc 579 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
46 | | solin 5256 |
. . . 4
⊢
((⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ (𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎)) |
47 | 33, 38, 45, 46 | syl12anc 866 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎)) |
48 | 13, 15, 26, 47 | mpjao3dan 1557 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
49 | | orc 894 |
. . . . 5
⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑎) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
50 | 49 | adantl 474 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
51 | 50, 24 | sylibr 226 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → 𝑏𝑇𝑎) |
52 | 51 | 3mix3d 1438 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
53 | | fnwe2.r |
. . . 4
⊢ (𝜑 → 𝑅 We 𝐵) |
54 | | weso 5303 |
. . . 4
⊢ (𝑅 We 𝐵 → 𝑅 Or 𝐵) |
55 | 53, 54 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 Or 𝐵) |
56 | | fvres 6430 |
. . . . 5
⊢ (𝑎 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑎) = (𝐹‘𝑎)) |
57 | 27, 56 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) = (𝐹‘𝑎)) |
58 | | fnwe2.f |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) |
59 | 58, 27 | ffvelrnd 6586 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) ∈ 𝐵) |
60 | 57, 59 | eqeltrrd 2879 |
. . 3
⊢ (𝜑 → (𝐹‘𝑎) ∈ 𝐵) |
61 | | fvres 6430 |
. . . . 5
⊢ (𝑏 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑏) = (𝐹‘𝑏)) |
62 | 39, 61 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) = (𝐹‘𝑏)) |
63 | 58, 39 | ffvelrnd 6586 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) ∈ 𝐵) |
64 | 62, 63 | eqeltrrd 2879 |
. . 3
⊢ (𝜑 → (𝐹‘𝑏) ∈ 𝐵) |
65 | | solin 5256 |
. . 3
⊢ ((𝑅 Or 𝐵 ∧ ((𝐹‘𝑎) ∈ 𝐵 ∧ (𝐹‘𝑏) ∈ 𝐵)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎))) |
66 | 55, 60, 64, 65 | syl12anc 866 |
. 2
⊢ (𝜑 → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎))) |
67 | 7, 48, 52, 66 | mpjao3dan 1557 |
1
⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |