Step | Hyp | Ref
| Expression |
1 | | f1otrg.h |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝑉) |
2 | | elex 3185 |
. . 3
⊢ (𝐻 ∈ 𝑉 → 𝐻 ∈ V) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝜑 → 𝐻 ∈ V) |
4 | | f1otrkg.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) |
5 | | f1ocnv 6062 |
. . . . . . . . . 10
⊢ (𝐹:𝐵–1-1-onto→𝑃 → ◡𝐹:𝑃–1-1-onto→𝐵) |
6 | | f1of 6050 |
. . . . . . . . . 10
⊢ (◡𝐹:𝑃–1-1-onto→𝐵 → ◡𝐹:𝑃⟶𝐵) |
7 | 4, 5, 6 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → ◡𝐹:𝑃⟶𝐵) |
8 | 7 | ad6antr 768 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ◡𝐹:𝑃⟶𝐵) |
9 | | simpllr 795 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑐 ∈ 𝑃) |
10 | 8, 9 | ffvelrnd 6268 |
. . . . . . 7
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (◡𝐹‘𝑐) ∈ 𝐵) |
11 | | simplr 788 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑑 ∈ 𝑃) |
12 | 8, 11 | ffvelrnd 6268 |
. . . . . . 7
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (◡𝐹‘𝑑) ∈ 𝐵) |
13 | | simpr1 1060 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐)) |
14 | 4 | ad3antrrr 762 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵–1-1-onto→𝑃) |
15 | 14 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝐹:𝐵–1-1-onto→𝑃) |
16 | | f1ocnvfv2 6433 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑐)) = 𝑐) |
17 | 15, 9, 16 | syl2anc 691 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(◡𝐹‘𝑐)) = 𝑐) |
18 | 17 | oveq2d 6565 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑐))) = ((𝐹‘𝑥)𝐼𝑐)) |
19 | 13, 18 | eleqtrrd 2691 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑐)))) |
20 | | f1otrkg.p |
. . . . . . . . 9
⊢ 𝑃 = (Base‘𝐺) |
21 | | f1otrkg.d |
. . . . . . . . 9
⊢ 𝐷 = (dist‘𝐺) |
22 | | f1otrkg.i |
. . . . . . . . 9
⊢ 𝐼 = (Itv‘𝐺) |
23 | | f1otrkg.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐻) |
24 | | f1otrkg.e |
. . . . . . . . 9
⊢ 𝐸 = (dist‘𝐻) |
25 | | f1otrkg.j |
. . . . . . . . 9
⊢ 𝐽 = (Itv‘𝐻) |
26 | | simp-4l 802 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢))) |
27 | | simplll 794 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
28 | | f1otrkg.1 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
29 | 28 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
30 | 27, 29 | sylancom 698 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
31 | 26, 30 | sylancom 698 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
32 | | simp-4l 802 |
. . . . . . . . . 10
⊢
((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢))) |
33 | | simplll 794 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) |
34 | | f1otrkg.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
35 | 34 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
36 | 33, 35 | sylancom 698 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
37 | 32, 36 | sylancom 698 |
. . . . . . . . 9
⊢
((((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
38 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
39 | 38 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ∈ 𝐵) |
40 | 39 | ad3antrrr 762 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑥 ∈ 𝐵) |
41 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
42 | 41 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑦 ∈ 𝐵) |
43 | 42 | ad3antrrr 762 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ 𝐵) |
44 | 20, 21, 22, 23, 24, 25, 15, 31, 37, 40, 10, 43 | f1otrgitv 25550 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑐)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑐))))) |
45 | 19, 44 | mpbird 246 |
. . . . . . 7
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑐))) |
46 | | simpr2 1061 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑)) |
47 | | f1ocnvfv2 6433 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑑 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑑)) = 𝑑) |
48 | 15, 11, 47 | syl2anc 691 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘(◡𝐹‘𝑑)) = 𝑑) |
49 | 48 | oveq2d 6565 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑑))) = ((𝐹‘𝑥)𝐼𝑑)) |
50 | 46, 49 | eleqtrrd 2691 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑑)))) |
51 | | simplr1 1096 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑧 ∈ 𝐵) |
52 | 51 | ad3antrrr 762 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ 𝐵) |
53 | 20, 21, 22, 23, 24, 25, 15, 31, 37, 40, 12, 52 | f1otrgitv 25550 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑧 ∈ (𝑥𝐽(◡𝐹‘𝑑)) ↔ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑑))))) |
54 | 50, 53 | mpbird 246 |
. . . . . . 7
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑧 ∈ (𝑥𝐽(◡𝐹‘𝑑))) |
55 | | simpr3 1062 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ (𝑐𝐼𝑑)) |
56 | 17, 48 | oveq12d 6567 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ((𝐹‘(◡𝐹‘𝑐))𝐼(𝐹‘(◡𝐹‘𝑑))) = (𝑐𝐼𝑑)) |
57 | 55, 56 | eleqtrrd 2691 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝐹‘𝑣) ∈ ((𝐹‘(◡𝐹‘𝑐))𝐼(𝐹‘(◡𝐹‘𝑑)))) |
58 | | simplr3 1098 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑣 ∈ 𝐵) |
59 | 58 | ad3antrrr 762 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ 𝐵) |
60 | 20, 21, 22, 23, 24, 25, 15, 31, 37, 10, 12, 59 | f1otrgitv 25550 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → (𝑣 ∈ ((◡𝐹‘𝑐)𝐽(◡𝐹‘𝑑)) ↔ (𝐹‘𝑣) ∈ ((𝐹‘(◡𝐹‘𝑐))𝐼(𝐹‘(◡𝐹‘𝑑))))) |
61 | 57, 60 | mpbird 246 |
. . . . . . 7
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → 𝑣 ∈ ((◡𝐹‘𝑐)𝐽(◡𝐹‘𝑑))) |
62 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑎 = (◡𝐹‘𝑐) → (𝑥𝐽𝑎) = (𝑥𝐽(◡𝐹‘𝑐))) |
63 | 62 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑎 = (◡𝐹‘𝑐) → (𝑦 ∈ (𝑥𝐽𝑎) ↔ 𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑐)))) |
64 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑎 = (◡𝐹‘𝑐) → (𝑎𝐽𝑏) = ((◡𝐹‘𝑐)𝐽𝑏)) |
65 | 64 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑎 = (◡𝐹‘𝑐) → (𝑣 ∈ (𝑎𝐽𝑏) ↔ 𝑣 ∈ ((◡𝐹‘𝑐)𝐽𝑏))) |
66 | 63, 65 | 3anbi13d 1393 |
. . . . . . . 8
⊢ (𝑎 = (◡𝐹‘𝑐) → ((𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((◡𝐹‘𝑐)𝐽𝑏)))) |
67 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑏 = (◡𝐹‘𝑑) → (𝑥𝐽𝑏) = (𝑥𝐽(◡𝐹‘𝑑))) |
68 | 67 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑏 = (◡𝐹‘𝑑) → (𝑧 ∈ (𝑥𝐽𝑏) ↔ 𝑧 ∈ (𝑥𝐽(◡𝐹‘𝑑)))) |
69 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑏 = (◡𝐹‘𝑑) → ((◡𝐹‘𝑐)𝐽𝑏) = ((◡𝐹‘𝑐)𝐽(◡𝐹‘𝑑))) |
70 | 69 | eleq2d 2673 |
. . . . . . . . 9
⊢ (𝑏 = (◡𝐹‘𝑑) → (𝑣 ∈ ((◡𝐹‘𝑐)𝐽𝑏) ↔ 𝑣 ∈ ((◡𝐹‘𝑐)𝐽(◡𝐹‘𝑑)))) |
71 | 68, 70 | 3anbi23d 1394 |
. . . . . . . 8
⊢ (𝑏 = (◡𝐹‘𝑑) → ((𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ ((◡𝐹‘𝑐)𝐽𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((◡𝐹‘𝑐)𝐽(◡𝐹‘𝑑))))) |
72 | 66, 71 | rspc2ev 3295 |
. . . . . . 7
⊢ (((◡𝐹‘𝑐) ∈ 𝐵 ∧ (◡𝐹‘𝑑) ∈ 𝐵 ∧ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑐)) ∧ 𝑧 ∈ (𝑥𝐽(◡𝐹‘𝑑)) ∧ 𝑣 ∈ ((◡𝐹‘𝑐)𝐽(◡𝐹‘𝑑)))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))) |
73 | 10, 12, 45, 54, 61, 72 | syl113anc 1330 |
. . . . . 6
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))) |
74 | | f1otrge.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈
TarskiGE) |
75 | 74 | ad3antrrr 762 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐺 ∈
TarskiGE) |
76 | | f1of 6050 |
. . . . . . . . . . 11
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃) |
77 | 4, 76 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐵⟶𝑃) |
78 | 77 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃) |
79 | 78, 38 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃) |
80 | 79 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ∈ 𝑃) |
81 | 78, 41 | ffvelrnd 6268 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃) |
82 | 81 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑦) ∈ 𝑃) |
83 | 77 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝐹:𝐵⟶𝑃) |
84 | 83, 51 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑧) ∈ 𝑃) |
85 | | simplr2 1097 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ 𝐵) |
86 | 83, 85 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ 𝑃) |
87 | 83, 58 | ffvelrnd 6268 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑣) ∈ 𝑃) |
88 | | simpr1 1060 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑥𝐽𝑣)) |
89 | 20, 21, 22, 23, 24, 25, 14, 30, 36, 39, 58, 85 | f1otrgitv 25550 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑥𝐽𝑣) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣)))) |
90 | 88, 89 | mpbid 221 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑣))) |
91 | | simpr2 1061 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑢 ∈ (𝑦𝐽𝑧)) |
92 | 20, 21, 22, 23, 24, 25, 14, 30, 36, 42, 51, 85 | f1otrgitv 25550 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝑢 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))) |
93 | 91, 92 | mpbid 221 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑢) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))) |
94 | 14, 39 | jca 553 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵)) |
95 | | simpr3 1062 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → 𝑥 ≠ 𝑢) |
96 | | dff1o6 6431 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢))) |
97 | 96 | simp3bi 1071 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢)) |
98 | 97 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢)) |
99 | 98 | r19.21bi 2916 |
. . . . . . . . . 10
⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑢) → 𝑥 = 𝑢)) |
100 | 99 | necon3d 2803 |
. . . . . . . . 9
⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → (𝑥 ≠ 𝑢 → (𝐹‘𝑥) ≠ (𝐹‘𝑢))) |
101 | 100 | imp 444 |
. . . . . . . 8
⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑥 ≠ 𝑢) → (𝐹‘𝑥) ≠ (𝐹‘𝑢)) |
102 | 94, 85, 95, 101 | syl21anc 1317 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → (𝐹‘𝑥) ≠ (𝐹‘𝑢)) |
103 | 20, 21, 22, 75, 80, 82, 84, 86, 87, 90, 93, 102 | axtgeucl 25171 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑐) ∧ (𝐹‘𝑧) ∈ ((𝐹‘𝑥)𝐼𝑑) ∧ (𝐹‘𝑣) ∈ (𝑐𝐼𝑑))) |
104 | 73, 103 | r19.29vva 3062 |
. . . . 5
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢)) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))) |
105 | 104 | ex 449 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))) |
106 | 105 | ralrimivvva 2955 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))) |
107 | 106 | ralrimivva 2954 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏)))) |
108 | 23, 24, 25 | istrkge 25156 |
. 2
⊢ (𝐻 ∈ TarskiGE
↔ (𝐻 ∈ V ∧
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑣) ∧ 𝑢 ∈ (𝑦𝐽𝑧) ∧ 𝑥 ≠ 𝑢) → ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑎) ∧ 𝑧 ∈ (𝑥𝐽𝑏) ∧ 𝑣 ∈ (𝑎𝐽𝑏))))) |
109 | 3, 107, 108 | sylanbrc 695 |
1
⊢ (𝜑 → 𝐻 ∈
TarskiGE) |