Proof of Theorem fnwe2lem3
Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . . . 5
⊢ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
2 | 1 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
3 | | fnwe2.su |
. . . . 5
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) |
4 | | fnwe2.t |
. . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} |
5 | 3, 4 | fnwe2val 36637 |
. . . 4
⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
6 | 2, 5 | sylibr 223 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → 𝑎𝑇𝑏) |
7 | 6 | 3mix1d 1229 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
8 | | simplr 788 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝐹‘𝑎) = (𝐹‘𝑏)) |
9 | | simpr 476 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) |
10 | 8, 9 | jca 553 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)) |
11 | 10 | olcd 407 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) |
12 | 11, 5 | sylibr 223 |
. . . 4
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎𝑇𝑏) |
13 | 12 | 3mix1d 1229 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
14 | | 3mix2 1224 |
. . . 4
⊢ (𝑎 = 𝑏 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
15 | 14 | adantl 481 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎 = 𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
16 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑎) = (𝐹‘𝑏)) |
17 | 16 | eqcomd 2616 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑏) = (𝐹‘𝑎)) |
18 | | csbeq1 3502 |
. . . . . . . . . 10
⊢ ((𝐹‘𝑎) = (𝐹‘𝑏) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆) |
19 | 18 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆) |
20 | 19 | breqd 4594 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎 ↔ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)) |
21 | 20 | biimpa 500 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎) |
22 | 17, 21 | jca 553 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)) |
23 | 22 | olcd 407 |
. . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
24 | 3, 4 | fnwe2val 36637 |
. . . . 5
⊢ (𝑏𝑇𝑎 ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
25 | 23, 24 | sylibr 223 |
. . . 4
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏𝑇𝑎) |
26 | 25 | 3mix3d 1231 |
. . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
27 | | fnwe2lem3.a |
. . . . . . 7
⊢ (𝜑 → 𝑎 ∈ 𝐴) |
28 | | fnwe2.s |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) |
29 | 3, 4, 28 | fnwe2lem1 36638 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
30 | 27, 29 | mpdan 699 |
. . . . . 6
⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
31 | | weso 5029 |
. . . . . 6
⊢
(⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
32 | 30, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
33 | 32 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
34 | 27 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ 𝐴) |
35 | | eqidd 2611 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑎)) |
36 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → (𝐹‘𝑦) = (𝐹‘𝑎)) |
37 | 36 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑎) = (𝐹‘𝑎))) |
38 | 37 | elrab 3331 |
. . . . 5
⊢ (𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ↔ (𝑎 ∈ 𝐴 ∧ (𝐹‘𝑎) = (𝐹‘𝑎))) |
39 | 34, 35, 38 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
40 | | fnwe2lem3.b |
. . . . . 6
⊢ (𝜑 → 𝑏 ∈ 𝐴) |
41 | 40 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ 𝐴) |
42 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑏)) |
43 | 42 | eqcomd 2616 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑏) = (𝐹‘𝑎)) |
44 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (𝐹‘𝑦) = (𝐹‘𝑏)) |
45 | 44 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑦 = 𝑏 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑏) = (𝐹‘𝑎))) |
46 | 45 | elrab 3331 |
. . . . 5
⊢ (𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ↔ (𝑏 ∈ 𝐴 ∧ (𝐹‘𝑏) = (𝐹‘𝑎))) |
47 | 41, 43, 46 | sylanbrc 695 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) |
48 | | solin 4982 |
. . . 4
⊢
((⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ (𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎)) |
49 | 33, 39, 47, 48 | syl12anc 1316 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎)) |
50 | 13, 15, 26, 49 | mpjao3dan 1387 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
51 | | orc 399 |
. . . . 5
⊢ ((𝐹‘𝑏)𝑅(𝐹‘𝑎) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
52 | 51 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) |
53 | 52, 24 | sylibr 223 |
. . 3
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → 𝑏𝑇𝑎) |
54 | 53 | 3mix3d 1231 |
. 2
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |
55 | | fnwe2.r |
. . . 4
⊢ (𝜑 → 𝑅 We 𝐵) |
56 | | weso 5029 |
. . . 4
⊢ (𝑅 We 𝐵 → 𝑅 Or 𝐵) |
57 | 55, 56 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 Or 𝐵) |
58 | | fvres 6117 |
. . . . 5
⊢ (𝑎 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑎) = (𝐹‘𝑎)) |
59 | 27, 58 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) = (𝐹‘𝑎)) |
60 | | fnwe2.f |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) |
61 | 60, 27 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) ∈ 𝐵) |
62 | 59, 61 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → (𝐹‘𝑎) ∈ 𝐵) |
63 | | fvres 6117 |
. . . . 5
⊢ (𝑏 ∈ 𝐴 → ((𝐹 ↾ 𝐴)‘𝑏) = (𝐹‘𝑏)) |
64 | 40, 63 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) = (𝐹‘𝑏)) |
65 | 60, 40 | ffvelrnd 6268 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) ∈ 𝐵) |
66 | 64, 65 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → (𝐹‘𝑏) ∈ 𝐵) |
67 | | solin 4982 |
. . 3
⊢ ((𝑅 Or 𝐵 ∧ ((𝐹‘𝑎) ∈ 𝐵 ∧ (𝐹‘𝑏) ∈ 𝐵)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎))) |
68 | 57, 62, 66, 67 | syl12anc 1316 |
. 2
⊢ (𝜑 → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎))) |
69 | 7, 50, 54, 68 | mpjao3dan 1387 |
1
⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |