Step | Hyp | Ref
| Expression |
1 | | fnwe2.f |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝐴):𝐴⟶𝐵) |
2 | | ffun 6548 |
. . . 4
⊢ ((𝐹 ↾ 𝐴):𝐴⟶𝐵 → Fun (𝐹 ↾ 𝐴)) |
3 | | vex 3412 |
. . . . 5
⊢ 𝑎 ∈ V |
4 | 3 | funimaex 6467 |
. . . 4
⊢ (Fun
(𝐹 ↾ 𝐴) → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V) |
5 | 1, 2, 4 | 3syl 18 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ∈ V) |
6 | | fnwe2.r |
. . . 4
⊢ (𝜑 → 𝑅 We 𝐵) |
7 | | wefr 5541 |
. . . 4
⊢ (𝑅 We 𝐵 → 𝑅 Fr 𝐵) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 Fr 𝐵) |
9 | | imassrn 5940 |
. . . 4
⊢ ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ ran (𝐹 ↾ 𝐴) |
10 | 1 | frnd 6553 |
. . . 4
⊢ (𝜑 → ran (𝐹 ↾ 𝐴) ⊆ 𝐵) |
11 | 9, 10 | sstrid 3912 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵) |
12 | | incom 4115 |
. . . . . 6
⊢ (dom
(𝐹 ↾ 𝐴) ∩ 𝑎) = (𝑎 ∩ dom (𝐹 ↾ 𝐴)) |
13 | | fnwe2lem2.a |
. . . . . . . 8
⊢ (𝜑 → 𝑎 ⊆ 𝐴) |
14 | 1 | fdmd 6556 |
. . . . . . . 8
⊢ (𝜑 → dom (𝐹 ↾ 𝐴) = 𝐴) |
15 | 13, 14 | sseqtrrd 3942 |
. . . . . . 7
⊢ (𝜑 → 𝑎 ⊆ dom (𝐹 ↾ 𝐴)) |
16 | | df-ss 3883 |
. . . . . . 7
⊢ (𝑎 ⊆ dom (𝐹 ↾ 𝐴) ↔ (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎) |
17 | 15, 16 | sylib 221 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∩ dom (𝐹 ↾ 𝐴)) = 𝑎) |
18 | 12, 17 | syl5eq 2790 |
. . . . 5
⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = 𝑎) |
19 | | fnwe2lem2.n0 |
. . . . 5
⊢ (𝜑 → 𝑎 ≠ ∅) |
20 | 18, 19 | eqnetrd 3008 |
. . . 4
⊢ (𝜑 → (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅) |
21 | | imadisj 5948 |
. . . . 5
⊢ (((𝐹 ↾ 𝐴) “ 𝑎) = ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) = ∅) |
22 | 21 | necon3bii 2993 |
. . . 4
⊢ (((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅ ↔ (dom (𝐹 ↾ 𝐴) ∩ 𝑎) ≠ ∅) |
23 | 20, 22 | sylibr 237 |
. . 3
⊢ (𝜑 → ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅) |
24 | | fri 5512 |
. . 3
⊢
(((((𝐹 ↾ 𝐴) “ 𝑎) ∈ V ∧ 𝑅 Fr 𝐵) ∧ (((𝐹 ↾ 𝐴) “ 𝑎) ⊆ 𝐵 ∧ ((𝐹 ↾ 𝐴) “ 𝑎) ≠ ∅)) → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑) |
25 | 5, 8, 11, 23, 24 | syl22anc 839 |
. 2
⊢ (𝜑 → ∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑) |
26 | | df-ima 5564 |
. . . . . 6
⊢ ((𝐹 ↾ 𝐴) “ 𝑎) = ran ((𝐹 ↾ 𝐴) ↾ 𝑎) |
27 | 26 | rexeqi 3324 |
. . . . 5
⊢
(∃𝑑 ∈
((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑) |
28 | 1 | ffnd 6546 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐴) Fn 𝐴) |
29 | | fnssres 6500 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝐴) Fn 𝐴 ∧ 𝑎 ⊆ 𝐴) → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎) |
30 | 28, 13, 29 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎) |
31 | | breq2 5057 |
. . . . . . . . 9
⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (𝑒𝑅𝑑 ↔ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
32 | 31 | notbid 321 |
. . . . . . . 8
⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (¬ 𝑒𝑅𝑑 ↔ ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
33 | 32 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑑 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
34 | 33 | rexrn 6906 |
. . . . . 6
⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
35 | 30, 34 | syl 17 |
. . . . 5
⊢ (𝜑 → (∃𝑑 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
36 | 27, 35 | syl5bb 286 |
. . . 4
⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
37 | 26 | raleqi 3323 |
. . . . . . . 8
⊢
(∀𝑒 ∈
((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓)) |
38 | | breq1 5056 |
. . . . . . . . . . 11
⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
39 | 38 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑒 = (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) → (¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
40 | 39 | ralrn 6907 |
. . . . . . . . 9
⊢ (((𝐹 ↾ 𝐴) ↾ 𝑎) Fn 𝑎 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
41 | 30, 40 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (∀𝑒 ∈ ran ((𝐹 ↾ 𝐴) ↾ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
42 | 37, 41 | syl5bb 286 |
. . . . . . 7
⊢ (𝜑 → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
43 | 42 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓))) |
44 | 13 | resabs1d 5882 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎)) |
45 | 44 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝐴) ↾ 𝑎) = (𝐹 ↾ 𝑎)) |
46 | 45 | fveq1d 6719 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = ((𝐹 ↾ 𝑎)‘𝑑)) |
47 | | fvres 6736 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑)) |
48 | 47 | adantl 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑑) = (𝐹‘𝑑)) |
49 | 46, 48 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑) = (𝐹‘𝑑)) |
50 | 45 | fveq1d 6719 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = ((𝐹 ↾ 𝑎)‘𝑓)) |
51 | | fvres 6736 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝑎 → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓)) |
52 | 51 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((𝐹 ↾ 𝑎)‘𝑓) = (𝐹‘𝑓)) |
53 | 50, 52 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) = (𝐹‘𝑓)) |
54 | 49, 53 | breq12d 5066 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → ((((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) |
55 | 54 | notbid 321 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑎) ∧ 𝑑 ∈ 𝑎) → (¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) |
56 | 55 | ralbidva 3117 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑑 ∈ 𝑎 ¬ (((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑑)𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) |
57 | 43, 56 | bitrd 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → (∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) |
58 | 57 | rexbidva 3215 |
. . . 4
⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅(((𝐹 ↾ 𝐴) ↾ 𝑎)‘𝑓) ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) |
59 | 36, 58 | bitrd 282 |
. . 3
⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 ↔ ∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) |
60 | 3 | inex1 5210 |
. . . . . . 7
⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V |
61 | 60 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V) |
62 | 13 | sselda 3901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → 𝑓 ∈ 𝐴) |
63 | | fnwe2.su |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘𝑥) → 𝑆 = 𝑈) |
64 | | fnwe2.t |
. . . . . . . . . 10
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝐹‘𝑥)𝑅(𝐹‘𝑦) ∨ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥𝑈𝑦))} |
65 | | fnwe2.s |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑈 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑥)}) |
66 | 63, 64, 65 | fnwe2lem1 40578 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) |
67 | | wefr 5541 |
. . . . . . . . 9
⊢
(⦋(𝐹‘𝑓) / 𝑧⦌𝑆 We {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) |
68 | 66, 67 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) |
69 | 62, 68 | syldan 594 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑎) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) |
70 | 69 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) |
71 | | inss2 4144 |
. . . . . . 7
⊢ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} |
72 | 71 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) |
73 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝑎) |
74 | | fveqeq2 6726 |
. . . . . . . . 9
⊢ (𝑦 = 𝑓 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑓) = (𝐹‘𝑓))) |
75 | 62 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ 𝐴) |
76 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝐹‘𝑓) = (𝐹‘𝑓)) |
77 | 74, 75, 76 | elrabd 3604 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) |
78 | 73, 77 | elind 4108 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → 𝑓 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})) |
79 | 78 | ne0d 4250 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅) |
80 | | fri 5512 |
. . . . . 6
⊢ ((((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∈ V ∧ ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 Fr {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ∧ ((𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ⊆ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ∧ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ≠ ∅)) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) |
81 | 61, 70, 72, 79, 80 | syl22anc 839 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) |
82 | | elin 3882 |
. . . . . . . 8
⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})) |
83 | | fveqeq2 6726 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑒 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑒) = (𝐹‘𝑓))) |
84 | 83 | elrab 3602 |
. . . . . . . . 9
⊢ (𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))) |
85 | 84 | anbi2i 626 |
. . . . . . . 8
⊢ ((𝑒 ∈ 𝑎 ∧ 𝑒 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) |
86 | 82, 85 | bitri 278 |
. . . . . . 7
⊢ (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) |
87 | | elin 3882 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})) |
88 | | fveqeq2 6726 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑔 → ((𝐹‘𝑦) = (𝐹‘𝑓) ↔ (𝐹‘𝑔) = (𝐹‘𝑓))) |
89 | 88 | elrab 3602 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)} ↔ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) |
90 | 89 | anbi2i 626 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ 𝑎 ∧ 𝑔 ∈ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)))) |
91 | 87, 90 | bitri 278 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ↔ (𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)))) |
92 | 91 | imbi1i 353 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) |
93 | | impexp 454 |
. . . . . . . . . . 11
⊢ (((𝑔 ∈ 𝑎 ∧ (𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓))) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))) |
94 | 92, 93 | bitri 278 |
. . . . . . . . . 10
⊢ ((𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ (𝑔 ∈ 𝑎 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))) |
95 | 94 | ralbii2 3086 |
. . . . . . . . 9
⊢
(∀𝑔 ∈
(𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) |
96 | | simplrl 777 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑒 ∈ 𝑎) |
97 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑐 → (𝐹‘𝑑) = (𝐹‘𝑐)) |
98 | 97 | breq1d 5063 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑐 → ((𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓))) |
99 | 98 | notbid 321 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝑐 → (¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) ↔ ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓))) |
100 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)) |
101 | 100 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓)) |
102 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝑎) |
103 | 99, 101, 102 | rspcdva 3539 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑓)) |
104 | | simprrr 782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (𝐹‘𝑒) = (𝐹‘𝑓)) |
105 | 104 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → (𝐹‘𝑒) = (𝐹‘𝑓)) |
106 | 105 | breq2d 5065 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ↔ (𝐹‘𝑐)𝑅(𝐹‘𝑓))) |
107 | 103, 106 | mtbird 328 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒)) |
108 | 13 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → 𝑎 ⊆ 𝐴) |
109 | 108 | sselda 3901 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → 𝑐 ∈ 𝐴) |
110 | 109 | adantrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝐴) |
111 | | simprr 773 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑒)) |
112 | 104 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑒) = (𝐹‘𝑓)) |
113 | 111, 112 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑐) = (𝐹‘𝑓)) |
114 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑐 → (𝑔 ∈ 𝐴 ↔ 𝑐 ∈ 𝐴)) |
115 | | fveqeq2 6726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑐 → ((𝐹‘𝑔) = (𝐹‘𝑓) ↔ (𝐹‘𝑐) = (𝐹‘𝑓))) |
116 | 114, 115 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑐 → ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) ↔ (𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)))) |
117 | | breq1 5056 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑐 → (𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) |
118 | 117 | notbid 321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑐 → (¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) |
119 | 116, 118 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = 𝑐 → (((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) ↔ ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒))) |
120 | | simplr 769 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) |
121 | | simprl 771 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → 𝑐 ∈ 𝑎) |
122 | 119, 120,
121 | rspcdva 3539 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ((𝑐 ∈ 𝐴 ∧ (𝐹‘𝑐) = (𝐹‘𝑓)) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) |
123 | 110, 113,
122 | mp2and 699 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) |
124 | 111, 112 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝐹‘𝑓) = (𝐹‘𝑐)) |
125 | 124 | csbeq1d 3815 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ⦋(𝐹‘𝑓) / 𝑧⦌𝑆 = ⦋(𝐹‘𝑐) / 𝑧⦌𝑆) |
126 | 125 | breqd 5064 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → (𝑐⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 ↔ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) |
127 | 123, 126 | mtbid 327 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ (𝑐 ∈ 𝑎 ∧ (𝐹‘𝑐) = (𝐹‘𝑒))) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒) |
128 | 127 | expr 460 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) |
129 | | imnan 403 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑐) = (𝐹‘𝑒) → ¬ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒) ↔ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) |
130 | 128, 129 | sylib 221 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) |
131 | | ioran 984 |
. . . . . . . . . . . . . 14
⊢ (¬
((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒)) ↔ (¬ (𝐹‘𝑐)𝑅(𝐹‘𝑒) ∧ ¬ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))) |
132 | 107, 130,
131 | sylanbrc 586 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))) |
133 | 63, 64 | fnwe2val 40577 |
. . . . . . . . . . . . 13
⊢ (𝑐𝑇𝑒 ↔ ((𝐹‘𝑐)𝑅(𝐹‘𝑒) ∨ ((𝐹‘𝑐) = (𝐹‘𝑒) ∧ 𝑐⦋(𝐹‘𝑐) / 𝑧⦌𝑆𝑒))) |
134 | 132, 133 | sylnibr 332 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) ∧ 𝑐 ∈ 𝑎) → ¬ 𝑐𝑇𝑒) |
135 | 134 | ralrimiva 3105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒) |
136 | | breq2 5057 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑒 → (𝑐𝑇𝑏 ↔ 𝑐𝑇𝑒)) |
137 | 136 | notbid 321 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑒 → (¬ 𝑐𝑇𝑏 ↔ ¬ 𝑐𝑇𝑒)) |
138 | 137 | ralbidv 3118 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝑒 → (∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏 ↔ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒)) |
139 | 138 | rspcev 3537 |
. . . . . . . . . . 11
⊢ ((𝑒 ∈ 𝑎 ∧ ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏) |
140 | 96, 135, 139 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) ∧ ∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒)) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏) |
141 | 140 | ex 416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ 𝑎 ((𝑔 ∈ 𝐴 ∧ (𝐹‘𝑔) = (𝐹‘𝑓)) → ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)) |
142 | 95, 141 | syl5bi 245 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) ∧ (𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓)))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)) |
143 | 142 | ex 416 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ((𝑒 ∈ 𝑎 ∧ (𝑒 ∈ 𝐴 ∧ (𝐹‘𝑒) = (𝐹‘𝑓))) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))) |
144 | 86, 143 | syl5bi 245 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) → (∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏))) |
145 | 144 | rexlimdv 3202 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → (∃𝑒 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)})∀𝑔 ∈ (𝑎 ∩ {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) = (𝐹‘𝑓)}) ¬ 𝑔⦋(𝐹‘𝑓) / 𝑧⦌𝑆𝑒 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)) |
146 | 81, 145 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ 𝑎 ∧ ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓))) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏) |
147 | 146 | rexlimdvaa 3204 |
. . 3
⊢ (𝜑 → (∃𝑓 ∈ 𝑎 ∀𝑑 ∈ 𝑎 ¬ (𝐹‘𝑑)𝑅(𝐹‘𝑓) → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)) |
148 | 59, 147 | sylbid 243 |
. 2
⊢ (𝜑 → (∃𝑑 ∈ ((𝐹 ↾ 𝐴) “ 𝑎)∀𝑒 ∈ ((𝐹 ↾ 𝐴) “ 𝑎) ¬ 𝑒𝑅𝑑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏)) |
149 | 25, 148 | mpd 15 |
1
⊢ (𝜑 → ∃𝑏 ∈ 𝑎 ∀𝑐 ∈ 𝑎 ¬ 𝑐𝑇𝑏) |