Proof of Theorem fnwe2lem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | animorrl 982 | . . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) | 
| 2 |  | fnwe2.su | . . . . 5
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) | 
| 3 |  | fnwe2.t | . . . . 5
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} | 
| 4 | 2, 3 | fnwe2val 43066 | . . . 4
⊢ (𝑎𝑇𝑏 ↔ ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) | 
| 5 | 1, 4 | sylibr 234 | . . 3
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → 𝑎𝑇𝑏) | 
| 6 | 5 | 3mix1d 1336 | . 2
⊢ ((𝜑 ∧ (𝐹‘𝑎)𝑅(𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | 
| 7 |  | simplr 768 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝐹‘𝑎) = (𝐹‘𝑏)) | 
| 8 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) | 
| 9 | 7, 8 | jca 511 | . . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏)) | 
| 10 | 9 | olcd 874 | . . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ ((𝐹‘𝑎) = (𝐹‘𝑏) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏))) | 
| 11 | 10, 4 | sylibr 234 | . . . 4
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → 𝑎𝑇𝑏) | 
| 12 | 11 | 3mix1d 1336 | . . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | 
| 13 |  | 3mix2 1331 | . . . 4
⊢ (𝑎 = 𝑏 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | 
| 14 | 13 | adantl 481 | . . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑎 = 𝑏) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | 
| 15 |  | simplr 768 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑎) = (𝐹‘𝑏)) | 
| 16 | 15 | eqcomd 2742 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝐹‘𝑏) = (𝐹‘𝑎)) | 
| 17 |  | csbeq1 3901 | . . . . . . . . . 10
⊢ ((𝐹‘𝑎) = (𝐹‘𝑏) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆) | 
| 18 | 17 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑏) / 𝑧⦌𝑆) | 
| 19 | 18 | breqd 5153 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎 ↔ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)) | 
| 20 | 19 | biimpa 476 | . . . . . . 7
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎) | 
| 21 | 16, 20 | jca 511 | . . . . . 6
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎)) | 
| 22 | 21 | olcd 874 | . . . . 5
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) | 
| 23 | 2, 3 | fnwe2val 43066 | . . . . 5
⊢ (𝑏𝑇𝑎 ↔ ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) | 
| 24 | 22, 23 | sylibr 234 | . . . 4
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → 𝑏𝑇𝑎) | 
| 25 | 24 | 3mix3d 1338 | . . 3
⊢ (((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ∧ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | 
| 26 |  | fnwe2lem3.a | . . . . . . 7
⊢ (𝜑 → 𝑎 ∈ 𝐴) | 
| 27 |  | fnwe2.s | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) | 
| 28 | 2, 3, 27 | fnwe2lem1 43067 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | 
| 29 | 26, 28 | mpdan 687 | . . . . . 6
⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | 
| 30 |  | weso 5675 | . . . . . 6
⊢
(⦋(𝐹‘𝑎) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | 
| 31 | 29, 30 | syl 17 | . . . . 5
⊢ (𝜑 → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | 
| 32 | 31 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | 
| 33 |  | fveqeq2 6914 | . . . . 5
⊢ (𝑦 = 𝑎 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑎) = (𝐹‘𝑎))) | 
| 34 | 26 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ 𝐴) | 
| 35 |  | eqidd 2737 | . . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑎)) | 
| 36 | 33, 34, 35 | elrabd 3693 | . . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | 
| 37 |  | fveqeq2 6914 | . . . . 5
⊢ (𝑦 = 𝑏 → ((𝐹‘𝑦) = (𝐹‘𝑎) ↔ (𝐹‘𝑏) = (𝐹‘𝑎))) | 
| 38 |  | fnwe2lem3.b | . . . . . 6
⊢ (𝜑 → 𝑏 ∈ 𝐴) | 
| 39 | 38 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ 𝐴) | 
| 40 |  | simpr 484 | . . . . . 6
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑎) = (𝐹‘𝑏)) | 
| 41 | 40 | eqcomd 2742 | . . . . 5
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝐹‘𝑏) = (𝐹‘𝑎)) | 
| 42 | 37, 39, 41 | elrabd 3693 | . . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)}) | 
| 43 |  | solin 5618 | . . . 4
⊢
((⦋(𝐹‘𝑎) / 𝑧⦌𝑆 Or {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ (𝑎 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)} ∧ 𝑏 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑎)})) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎)) | 
| 44 | 32, 36, 42, 43 | syl12anc 836 | . . 3
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏⦋(𝐹‘𝑎) / 𝑧⦌𝑆𝑎)) | 
| 45 | 12, 14, 25, 44 | mpjao3dan 1433 | . 2
⊢ ((𝜑 ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | 
| 46 |  | animorrl 982 | . . . 4
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → ((𝐹‘𝑏)𝑅(𝐹‘𝑎) ∨ ((𝐹‘𝑏) = (𝐹‘𝑎) ∧ 𝑏⦋(𝐹‘𝑏) / 𝑧⦌𝑆𝑎))) | 
| 47 | 46, 23 | sylibr 234 | . . 3
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → 𝑏𝑇𝑎) | 
| 48 | 47 | 3mix3d 1338 | . 2
⊢ ((𝜑 ∧ (𝐹‘𝑏)𝑅(𝐹‘𝑎)) → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) | 
| 49 |  | fnwe2.r | . . . 4
⊢ (𝜑 → 𝑅 We 𝐵) | 
| 50 |  | weso 5675 | . . . 4
⊢ (𝑅 We 𝐵 → 𝑅 Or 𝐵) | 
| 51 | 49, 50 | syl 17 | . . 3
⊢ (𝜑 → 𝑅 Or 𝐵) | 
| 52 | 26 | fvresd 6925 | . . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) = (𝐹‘𝑎)) | 
| 53 |  | fnwe2.f | . . . . 5
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) | 
| 54 | 53, 26 | ffvelcdmd 7104 | . . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑎) ∈ 𝐵) | 
| 55 | 52, 54 | eqeltrrd 2841 | . . 3
⊢ (𝜑 → (𝐹‘𝑎) ∈ 𝐵) | 
| 56 | 38 | fvresd 6925 | . . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) = (𝐹‘𝑏)) | 
| 57 | 53, 38 | ffvelcdmd 7104 | . . . 4
⊢ (𝜑 → ((𝐹 ↾ 𝐴)‘𝑏) ∈ 𝐵) | 
| 58 | 56, 57 | eqeltrrd 2841 | . . 3
⊢ (𝜑 → (𝐹‘𝑏) ∈ 𝐵) | 
| 59 |  | solin 5618 | . . 3
⊢ ((𝑅 Or 𝐵 ∧ ((𝐹‘𝑎) ∈ 𝐵 ∧ (𝐹‘𝑏) ∈ 𝐵)) → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎))) | 
| 60 | 51, 55, 58, 59 | syl12anc 836 | . 2
⊢ (𝜑 → ((𝐹‘𝑎)𝑅(𝐹‘𝑏) ∨ (𝐹‘𝑎) = (𝐹‘𝑏) ∨ (𝐹‘𝑏)𝑅(𝐹‘𝑎))) | 
| 61 | 6, 45, 48, 60 | mpjao3dan 1433 | 1
⊢ (𝜑 → (𝑎𝑇𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑇𝑎)) |