Step | Hyp | Ref
| Expression |
1 | | f1otrg.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ 𝑉) |
2 | | elex 3185 |
. . . . . 6
⊢ (𝐻 ∈ 𝑉 → 𝐻 ∈ V) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ V) |
4 | | f1otrkg.p |
. . . . . . . . 9
⊢ 𝑃 = (Base‘𝐺) |
5 | | f1otrkg.d |
. . . . . . . . 9
⊢ 𝐷 = (dist‘𝐺) |
6 | | f1otrkg.i |
. . . . . . . . 9
⊢ 𝐼 = (Itv‘𝐺) |
7 | | f1otrg.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
8 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ TarskiG) |
9 | | f1otrkg.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) |
10 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐵⟶𝑃) |
12 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃) |
13 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
14 | 12, 13 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃) |
15 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
16 | 12, 15 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃) |
17 | 4, 5, 6, 8, 14, 16 | axtgcgrrflx 25161 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑦)𝐷(𝐹‘𝑥))) |
18 | | f1otrkg.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐻) |
19 | | f1otrkg.e |
. . . . . . . . 9
⊢ 𝐸 = (dist‘𝐻) |
20 | | f1otrkg.j |
. . . . . . . . 9
⊢ 𝐽 = (Itv‘𝐻) |
21 | 9 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝑃) |
22 | | f1otrkg.1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
23 | 22 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
24 | | f1otrkg.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
25 | 24 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
26 | 4, 5, 6, 18, 19, 20, 21, 23, 25, 13, 15 | f1otrgds 25549 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦))) |
27 | 4, 5, 6, 18, 19, 20, 21, 23, 25, 15, 13 | f1otrgds 25549 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦𝐸𝑥) = ((𝐹‘𝑦)𝐷(𝐹‘𝑥))) |
28 | 17, 26, 27 | 3eqtr4d 2654 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥)) |
29 | 28 | ralrimivva 2954 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥)) |
30 | | f1of1 6049 |
. . . . . . . . . . 11
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵–1-1→𝑃) |
31 | 9, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐵–1-1→𝑃) |
32 | 31 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵–1-1→𝑃) |
33 | | simp21 1087 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 ∈ 𝐵) |
34 | | simp22 1088 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦 ∈ 𝐵) |
35 | 33, 34 | jca 553 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
36 | 7 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG) |
37 | 11 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵⟶𝑃) |
38 | 37, 33 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑥) ∈ 𝑃) |
39 | 37, 34 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑦) ∈ 𝑃) |
40 | | simp23 1089 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧 ∈ 𝐵) |
41 | 37, 40 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑧) ∈ 𝑃) |
42 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) |
43 | 9 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵–1-1-onto→𝑃) |
44 | 22 | 3ad2antl1 1216 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
45 | 24 | 3ad2antl1 1216 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
46 | 4, 5, 6, 18, 19, 20, 43, 44, 45, 33, 34 | f1otrgds 25549 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦))) |
47 | 4, 5, 6, 18, 19, 20, 43, 44, 45, 40, 40 | f1otrgds 25549 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹‘𝑧)𝐷(𝐹‘𝑧))) |
48 | 42, 46, 47 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑧)𝐷(𝐹‘𝑧))) |
49 | 4, 5, 6, 36, 38, 39, 41, 48 | axtgcgrid 25162 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
50 | | f1veqaeq 6418 |
. . . . . . . . . 10
⊢ ((𝐹:𝐵–1-1→𝑃 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
51 | 50 | imp 444 |
. . . . . . . . 9
⊢ (((𝐹:𝐵–1-1→𝑃 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 = 𝑦) |
52 | 32, 35, 49, 51 | syl21anc 1317 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦) |
53 | 52 | 3expia 1259 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)) |
54 | 53 | ralrimivvva 2955 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)) |
55 | 29, 54 | jca 553 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))) |
56 | 18, 19, 20 | istrkgc 25153 |
. . . . 5
⊢ (𝐻 ∈ TarskiGC
↔ (𝐻 ∈ V ∧
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))) |
57 | 3, 55, 56 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → 𝐻 ∈
TarskiGC) |
58 | 9 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵–1-1-onto→𝑃) |
59 | 58, 30 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵–1-1→𝑃) |
60 | | simp2 1055 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
61 | 7 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG) |
62 | 14 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑥) ∈ 𝑃) |
63 | 16 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑦) ∈ 𝑃) |
64 | | simp3 1056 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥)) |
65 | 22 | 3ad2antl1 1216 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
66 | 24 | 3ad2antl1 1216 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
67 | 13 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 ∈ 𝐵) |
68 | 15 | 3adant3 1074 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ 𝐵) |
69 | 4, 5, 6, 18, 19, 20, 58, 65, 66, 67, 67, 68 | f1otrgitv 25550 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑥)))) |
70 | 64, 69 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑥))) |
71 | 4, 5, 6, 61, 62, 63, 70 | axtgbtwnid 25165 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
72 | 59, 60, 71, 51 | syl21anc 1317 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦) |
73 | 72 | 3expia 1259 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦)) |
74 | 73 | ralrimivva 2954 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦)) |
75 | | f1ocnv 6062 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐵–1-1-onto→𝑃 → ◡𝐹:𝑃–1-1-onto→𝐵) |
76 | | f1of 6050 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹:𝑃–1-1-onto→𝐵 → ◡𝐹:𝑃⟶𝐵) |
77 | 9, 75, 76 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ◡𝐹:𝑃⟶𝐵) |
78 | 77 | ad5antr 766 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ◡𝐹:𝑃⟶𝐵) |
79 | | simplr 788 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ 𝑃) |
80 | 78, 79 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (◡𝐹‘𝑐) ∈ 𝐵) |
81 | | simpr 476 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → 𝑎 = (◡𝐹‘𝑐)) |
82 | 81 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦))) |
83 | 81 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥))) |
84 | 82, 83 | anbi12d 743 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ∧ (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥)))) |
85 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦))) |
86 | 21 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵–1-1-onto→𝑃) |
87 | 86 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝐹:𝐵–1-1-onto→𝑃) |
88 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑐)) = 𝑐) |
89 | 88 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ↔ 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))) |
90 | 87, 79, 89 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ↔ 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))) |
91 | 85, 90 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦))) |
92 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)))) |
93 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
94 | 93, 23 | sylancom 698 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
95 | 92, 94 | sylancom 698 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
96 | | simplll 794 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)))) |
97 | | simplll 794 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
98 | 97, 25 | sylancom 698 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
99 | 96, 98 | sylancom 698 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
100 | | simplr2 1097 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ 𝐵) |
101 | 100 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑢 ∈ 𝐵) |
102 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦 ∈ 𝐵) |
103 | 102 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑦 ∈ 𝐵) |
104 | 4, 5, 6, 18, 19, 20, 87, 95, 99, 101, 103, 80 | f1otrgitv 25550 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))) |
105 | 91, 104 | mpbird 246 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦)) |
106 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))) |
107 | 88 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)) ↔ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
108 | 87, 79, 107 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)) ↔ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
109 | 106, 108 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))) |
110 | | simplr3 1098 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ 𝐵) |
111 | 110 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑣 ∈ 𝐵) |
112 | 13 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥 ∈ 𝐵) |
113 | 112 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑥 ∈ 𝐵) |
114 | 4, 5, 6, 18, 19, 20, 87, 95, 99, 111, 113, 80 | f1otrgitv 25550 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
115 | 109, 114 | mpbird 246 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥)) |
116 | 105, 115 | jca 553 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ∧ (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥))) |
117 | 80, 84, 116 | rspcedvd 3289 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) |
118 | 8 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG) |
119 | 12 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵⟶𝑃) |
120 | 119, 112 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑥) ∈ 𝑃) |
121 | 119, 102 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑦) ∈ 𝑃) |
122 | | simplr1 1096 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧 ∈ 𝐵) |
123 | 119, 122 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑧) ∈ 𝑃) |
124 | 119, 100 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑢) ∈ 𝑃) |
125 | 119, 110 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑣) ∈ 𝑃) |
126 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧)) |
127 | 4, 5, 6, 18, 19, 20, 86, 94, 98, 112, 122, 100 | f1otrgitv 25550 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧)))) |
128 | 126, 127 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧))) |
129 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧)) |
130 | 4, 5, 6, 18, 19, 20, 86, 94, 98, 102, 122, 110 | f1otrgitv 25550 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑣) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))) |
131 | 129, 130 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑣) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))) |
132 | 4, 5, 6, 118, 120, 121, 123, 124, 125, 128, 131 | axtgpasch 25166 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐 ∈ 𝑃 (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
133 | 117, 132 | r19.29a 3060 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) |
134 | 133 | ex 449 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))) |
135 | 134 | ralrimivvva 2955 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))) |
136 | 135 | ralrimivva 2954 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))) |
137 | 9 | ad5antr 766 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃) |
138 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ 𝑃) |
139 | 137, 138,
88 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘(◡𝐹‘𝑐)) = 𝑐) |
140 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝐵⟶𝑃 → 𝐹 Fn 𝐵) |
141 | 137, 10, 140 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹 Fn 𝐵) |
142 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) |
143 | 142 | simpld 474 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ∈ 𝒫 𝐵) |
144 | 143 | elpwid 4118 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ 𝐵) |
145 | 144 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ 𝐵) |
146 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠) |
147 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐵 ∧ 𝑠 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑠) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑠)) |
148 | 141, 145,
146, 147 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑠)) |
149 | 142 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ∈ 𝒫 𝐵) |
150 | 149 | elpwid 4118 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ 𝐵) |
151 | 150 | adantlr 747 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ 𝐵) |
152 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡) |
153 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 Fn 𝐵 ∧ 𝑡 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑡) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑡)) |
154 | 141, 151,
152, 153 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑡)) |
155 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) |
156 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = (𝐹‘𝑥) → (𝑒𝐼𝑓) = ((𝐹‘𝑥)𝐼𝑓)) |
157 | 156 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝐹‘𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹‘𝑥)𝐼𝑓))) |
158 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝐹‘𝑦) → ((𝐹‘𝑥)𝐼𝑓) = ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
159 | 158 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐹‘𝑦) → (𝑐 ∈ ((𝐹‘𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))) |
160 | 157, 159 | rspc2va 3294 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐹‘𝑥) ∈ (𝐹 “ 𝑠) ∧ (𝐹‘𝑦) ∈ (𝐹 “ 𝑡)) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
161 | 148, 154,
155, 160 | syl21anc 1317 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
162 | 139, 161 | eqeltrd 2688 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
163 | 9 | ad4antr 764 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃) |
164 | | simp-5l 804 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → 𝜑) |
165 | 164, 22 | sylancom 698 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
166 | | simp-5l 804 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝜑) |
167 | 166, 24 | sylancom 698 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
168 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠) |
169 | 144, 168 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝐵) |
170 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡) |
171 | 150, 170 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝐵) |
172 | 77 | ad4antr 764 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ◡𝐹:𝑃⟶𝐵) |
173 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ 𝑃) |
174 | 172, 173 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (◡𝐹‘𝑐) ∈ 𝐵) |
175 | 4, 5, 6, 18, 19, 20, 163, 165, 167, 169, 171, 174 | f1otrgitv 25550 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ((◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))) |
176 | 175 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ((◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))) |
177 | 162, 176 | mpbird 246 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)) |
178 | 177 | ralrimivva 2954 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)) |
179 | 178 | adantllr 751 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)) |
180 | 77 | ad4antr 764 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → ◡𝐹:𝑃⟶𝐵) |
181 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ 𝑃) |
182 | 180, 181 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → (◡𝐹‘𝑐) ∈ 𝐵) |
183 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (◡𝐹‘𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))) |
184 | 183 | 2ralbidv 2972 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (◡𝐹‘𝑐) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))) |
185 | 184 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 = (◡𝐹‘𝑐)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))) |
186 | 182, 185 | rspcedv 3286 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
187 | 186 | adantr 480 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
188 | 179, 187 | mpd 15 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)) |
189 | 7 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG) |
190 | | imassrn 5396 |
. . . . . . . . . . . 12
⊢ (𝐹 “ 𝑠) ⊆ ran 𝐹 |
191 | | f1ofo 6057 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵–onto→𝑃) |
192 | | forn 6031 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐵–onto→𝑃 → ran 𝐹 = 𝑃) |
193 | 9, 191, 192 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ran 𝐹 = 𝑃) |
194 | 193 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃) |
195 | 190, 194 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹 “ 𝑠) ⊆ 𝑃) |
196 | | imassrn 5396 |
. . . . . . . . . . . 12
⊢ (𝐹 “ 𝑡) ⊆ ran 𝐹 |
197 | 196, 194 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹 “ 𝑡) ⊆ 𝑃) |
198 | 11 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵⟶𝑃) |
199 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎 ∈ 𝐵) |
200 | 198, 199 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹‘𝑎) ∈ 𝑃) |
201 | 9 | ad5antr 766 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃) |
202 | | ffn 5958 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡𝐹:𝑃⟶𝐵 → ◡𝐹 Fn 𝑃) |
203 | 201, 75, 76, 202 | 4syl 19 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ◡𝐹 Fn 𝑃) |
204 | 195 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹 “ 𝑠) ⊆ 𝑃) |
205 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ (𝐹 “ 𝑠)) |
206 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐹 Fn 𝑃 ∧ (𝐹 “ 𝑠) ⊆ 𝑃 ∧ 𝑢 ∈ (𝐹 “ 𝑠)) → (◡𝐹‘𝑢) ∈ (◡𝐹 “ (𝐹 “ 𝑠))) |
207 | 203, 204,
205, 206 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ (◡𝐹 “ (𝐹 “ 𝑠))) |
208 | 201, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝐹:𝐵–1-1→𝑃) |
209 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) |
210 | 209 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑠 ∈ 𝒫 𝐵) |
211 | 210 | elpwid 4118 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑠 ⊆ 𝐵) |
212 | | f1imacnv 6066 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝐵–1-1→𝑃 ∧ 𝑠 ⊆ 𝐵) → (◡𝐹 “ (𝐹 “ 𝑠)) = 𝑠) |
213 | 208, 211,
212 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹 “ (𝐹 “ 𝑠)) = 𝑠) |
214 | 207, 213 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ 𝑠) |
215 | 197 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹 “ 𝑡) ⊆ 𝑃) |
216 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑣 ∈ (𝐹 “ 𝑡)) |
217 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . 17
⊢ ((◡𝐹 Fn 𝑃 ∧ (𝐹 “ 𝑡) ⊆ 𝑃 ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ (◡𝐹 “ (𝐹 “ 𝑡))) |
218 | 203, 215,
216, 217 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ (◡𝐹 “ (𝐹 “ 𝑡))) |
219 | 209 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑡 ∈ 𝒫 𝐵) |
220 | 219 | elpwid 4118 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑡 ⊆ 𝐵) |
221 | | f1imacnv 6066 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹:𝐵–1-1→𝑃 ∧ 𝑡 ⊆ 𝐵) → (◡𝐹 “ (𝐹 “ 𝑡)) = 𝑡) |
222 | 208, 220,
221 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹 “ (𝐹 “ 𝑡)) = 𝑡) |
223 | 218, 222 | eleqtrd 2690 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ 𝑡) |
224 | | simpllr 795 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) |
225 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (◡𝐹‘𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (◡𝐹‘𝑢) ∈ (𝑎𝐽𝑦))) |
226 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (◡𝐹‘𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(◡𝐹‘𝑣))) |
227 | 226 | eleq2d 2673 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (◡𝐹‘𝑣) → ((◡𝐹‘𝑢) ∈ (𝑎𝐽𝑦) ↔ (◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣)))) |
228 | 225, 227 | rspc2va 3294 |
. . . . . . . . . . . . . . 15
⊢ ((((◡𝐹‘𝑢) ∈ 𝑠 ∧ (◡𝐹‘𝑣) ∈ 𝑡) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣))) |
229 | 214, 223,
224, 228 | syl21anc 1317 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣))) |
230 | | simp-6l 806 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → 𝜑) |
231 | 230, 22 | sylancom 698 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
232 | | simp-6l 806 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝜑) |
233 | 232, 24 | sylancom 698 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
234 | | simp-4r 803 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑎 ∈ 𝐵) |
235 | 215, 216 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑣 ∈ 𝑃) |
236 | | f1ocnvdm 6440 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) → (◡𝐹‘𝑣) ∈ 𝐵) |
237 | 201, 235,
236 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ 𝐵) |
238 | 204, 205 | sseldd 3569 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ 𝑃) |
239 | | f1ocnvdm 6440 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑢 ∈ 𝑃) → (◡𝐹‘𝑢) ∈ 𝐵) |
240 | 201, 238,
239 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ 𝐵) |
241 | 4, 5, 6, 18, 19, 20, 201, 231, 233, 234, 237, 240 | f1otrgitv 25550 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ((◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣)) ↔ (𝐹‘(◡𝐹‘𝑢)) ∈ ((𝐹‘𝑎)𝐼(𝐹‘(◡𝐹‘𝑣))))) |
242 | 229, 241 | mpbid 221 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(◡𝐹‘𝑢)) ∈ ((𝐹‘𝑎)𝐼(𝐹‘(◡𝐹‘𝑣)))) |
243 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑢 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑢)) = 𝑢) |
244 | 201, 238,
243 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(◡𝐹‘𝑢)) = 𝑢) |
245 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑣)) = 𝑣) |
246 | 201, 235,
245 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(◡𝐹‘𝑣)) = 𝑣) |
247 | 246 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ((𝐹‘𝑎)𝐼(𝐹‘(◡𝐹‘𝑣))) = ((𝐹‘𝑎)𝐼𝑣)) |
248 | 242, 244,
247 | 3eltr3d 2702 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ ((𝐹‘𝑎)𝐼𝑣)) |
249 | 248 | 3impa 1251 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ ((𝐹‘𝑎)𝐼𝑣)) |
250 | 4, 5, 6, 189, 195, 197, 200, 249 | axtgcont 25168 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐 ∈ 𝑃 ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) |
251 | 188, 250 | r19.29a 3060 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)) |
252 | 251 | r19.29an 3059 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ ∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)) |
253 | 252 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
254 | 253 | ralrimivva 2954 |
. . . . . 6
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
255 | 74, 136, 254 | 3jca 1235 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)))) |
256 | 18, 19, 20 | istrkgb 25154 |
. . . . 5
⊢ (𝐻 ∈ TarskiGB
↔ (𝐻 ∈ V ∧
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))))) |
257 | 3, 255, 256 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → 𝐻 ∈
TarskiGB) |
258 | 57, 257 | elind 3760 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (TarskiGC ∩
TarskiGB)) |
259 | 7 | ad9antr 774 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG) |
260 | 11 | ad9antr 774 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵⟶𝑃) |
261 | | simp-9r 813 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥 ∈ 𝐵) |
262 | 260, 261 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑥) ∈ 𝑃) |
263 | | simp-8r 811 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ 𝐵) |
264 | 260, 263 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑦) ∈ 𝑃) |
265 | | simp-7r 809 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧 ∈ 𝐵) |
266 | 260, 265 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑧) ∈ 𝑃) |
267 | | simp-5r 805 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎 ∈ 𝐵) |
268 | 260, 267 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑎) ∈ 𝑃) |
269 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ 𝐵) |
270 | 260, 269 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑏) ∈ 𝑃) |
271 | | simpllr 795 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐 ∈ 𝐵) |
272 | 260, 271 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑐) ∈ 𝑃) |
273 | | simp-6r 807 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢 ∈ 𝐵) |
274 | 260, 273 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑢) ∈ 𝑃) |
275 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣 ∈ 𝐵) |
276 | 260, 275 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑣) ∈ 𝑃) |
277 | 9 | ad9antr 774 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵–1-1-onto→𝑃) |
278 | 277, 261 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵)) |
279 | | simprl1 1099 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥 ≠ 𝑦) |
280 | | dff1o6 6431 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
281 | 280 | simp3bi 1071 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
282 | 281 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
283 | 282 | r19.21bi 2916 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
284 | 283 | necon3d 2803 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥 ≠ 𝑦 → (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
285 | 284 | imp 444 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ≠ 𝑦) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
286 | 278, 263,
279, 285 | syl21anc 1317 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
287 | | simprl2 1100 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧)) |
288 | 22 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))) |
289 | 288 | ad9antr 774 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))) |
290 | 289 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
291 | 24 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))) |
292 | 291 | ad9antr 774 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))) |
293 | 292 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
294 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 261, 265, 263 | f1otrgitv 25550 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧)))) |
295 | 287, 294 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧))) |
296 | | simprl3 1101 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐)) |
297 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 267, 271, 269 | f1otrgitv 25550 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹‘𝑏) ∈ ((𝐹‘𝑎)𝐼(𝐹‘𝑐)))) |
298 | 296, 297 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑏) ∈ ((𝐹‘𝑎)𝐼(𝐹‘𝑐))) |
299 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) |
300 | 299 | simpld 474 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐))) |
301 | 300 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏)) |
302 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 261, 263 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦))) |
303 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 267, 269 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
304 | 301, 302,
303 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
305 | 300 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) |
306 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 263, 265 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹‘𝑦)𝐷(𝐹‘𝑧))) |
307 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 269, 271 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹‘𝑏)𝐷(𝐹‘𝑐))) |
308 | 305, 306,
307 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑦)𝐷(𝐹‘𝑧)) = ((𝐹‘𝑏)𝐷(𝐹‘𝑐))) |
309 | 299 | simprd 478 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))) |
310 | 309 | simpld 474 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣)) |
311 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 261, 273 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹‘𝑥)𝐷(𝐹‘𝑢))) |
312 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 267, 275 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹‘𝑎)𝐷(𝐹‘𝑣))) |
313 | 310, 311,
312 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑥)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑣))) |
314 | 309 | simprd 478 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣)) |
315 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 263, 273 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹‘𝑦)𝐷(𝐹‘𝑢))) |
316 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 269, 275 | f1otrgds 25549 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹‘𝑏)𝐷(𝐹‘𝑣))) |
317 | 314, 315,
316 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑦)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑏)𝐷(𝐹‘𝑣))) |
318 | 4, 5, 6, 259, 262, 264, 266, 268, 270, 272, 274, 276, 286, 295, 298, 304, 308, 313, 317 | axtg5seg 25164 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑧)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑐)𝐷(𝐹‘𝑣))) |
319 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 265, 273 | f1otrgds 25549 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹‘𝑧)𝐷(𝐹‘𝑢))) |
320 | 4, 5, 6, 18, 19, 20, 277, 290, 293, 271, 275 | f1otrgds 25549 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹‘𝑐)𝐷(𝐹‘𝑣))) |
321 | 318, 319,
320 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) |
322 | 321 | ex 449 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
323 | 322 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
324 | 323 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
325 | 324 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
326 | 325 | ralrimiva 2949 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
327 | 326 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
328 | 327 | ralrimiva 2949 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
329 | 328 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
330 | 329 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
331 | | simp-4l 802 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝜑) |
332 | | simplr 788 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑤 ∈ 𝑃) |
333 | | simprl 790 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤)) |
334 | 331, 9 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝐹:𝐵–1-1-onto→𝑃) |
335 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑤 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑤)) = 𝑤) |
336 | 334, 332,
335 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘(◡𝐹‘𝑤)) = 𝑤) |
337 | 336 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑤))) = ((𝐹‘𝑥)𝐼𝑤)) |
338 | 333, 337 | eleqtrrd 2691 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑤)))) |
339 | 331, 22 | sylan 487 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
340 | 331, 24 | sylan 487 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
341 | 13 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑥 ∈ 𝐵) |
342 | 77 | ffvelrnda 6267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑃) → (◡𝐹‘𝑤) ∈ 𝐵) |
343 | 331, 332,
342 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (◡𝐹‘𝑤) ∈ 𝐵) |
344 | 15 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑦 ∈ 𝐵) |
345 | 4, 5, 6, 18, 19, 20, 334, 339, 340, 341, 343, 344 | f1otrgitv 25550 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑤))))) |
346 | 338, 345 | mpbird 246 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤))) |
347 | 4, 5, 6, 18, 19, 20, 334, 339, 340, 344, 343 | f1otrgds 25549 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(◡𝐹‘𝑤)) = ((𝐹‘𝑦)𝐷(𝐹‘(◡𝐹‘𝑤)))) |
348 | 336 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑦)𝐷(𝐹‘(◡𝐹‘𝑤))) = ((𝐹‘𝑦)𝐷𝑤)) |
349 | | simprr 792 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
350 | 347, 348,
349 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(◡𝐹‘𝑤)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
351 | | simprl 790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
352 | 351 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑎 ∈ 𝐵) |
353 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
354 | 353 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑏 ∈ 𝐵) |
355 | 4, 5, 6, 18, 19, 20, 334, 339, 340, 352, 354 | f1otrgds 25549 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑎𝐸𝑏) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
356 | 350, 355 | eqtr4d 2647 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)) |
357 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (◡𝐹‘𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(◡𝐹‘𝑤))) |
358 | 357 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (◡𝐹‘𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)))) |
359 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (◡𝐹‘𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(◡𝐹‘𝑤))) |
360 | 359 | eqeq1d 2612 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (◡𝐹‘𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏))) |
361 | 358, 360 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (◡𝐹‘𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)))) |
362 | 361 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑃) ∧ 𝑧 = (◡𝐹‘𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)))) |
363 | 342, 362 | rspcedv 3286 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑃) → ((𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))) |
364 | 363 | imp 444 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑃) ∧ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
365 | 331, 332,
346, 356, 364 | syl22anc 1319 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
366 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐺 ∈ TarskiG) |
367 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃) |
368 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃) |
369 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃) |
370 | 369, 351 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑎) ∈ 𝑃) |
371 | 369, 353 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) ∈ 𝑃) |
372 | 4, 5, 6, 366, 367, 368, 370, 371 | axtgsegcon 25163 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑤 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) |
373 | 365, 372 | r19.29a 3060 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
374 | 373 | ralrimivva 2954 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
375 | 374 | ralrimivva 2954 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
376 | 3, 330, 375 | jca32 556 |
. . . . 5
⊢ (𝜑 → (𝐻 ∈ V ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))) |
377 | 18, 19, 20 | istrkgcb 25155 |
. . . . 5
⊢ (𝐻 ∈ TarskiGCB
↔ (𝐻 ∈ V ∧
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))) |
378 | 376, 377 | sylibr 223 |
. . . 4
⊢ (𝜑 → 𝐻 ∈
TarskiGCB) |
379 | | f1otrg.l |
. . . . 5
⊢ (𝜑 → (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})) |
380 | 18, 19, 20 | istrkgl 25157 |
. . . . 5
⊢ (𝐻 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))) |
381 | 3, 379, 380 | sylanbrc 695 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) |
382 | 378, 381 | elind 3760 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (TarskiGCB ∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
383 | 258, 382 | elind 3760 |
. 2
⊢ (𝜑 → 𝐻 ∈ ((TarskiGC ∩
TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))) |
384 | | df-trkg 25152 |
. 2
⊢ TarskiG =
((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB
∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
385 | 383, 384 | syl6eleqr 2699 |
1
⊢ (𝜑 → 𝐻 ∈ TarskiG) |