| Step | Hyp | Ref
| Expression |
| 1 | | f1otrg.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ 𝑉) |
| 2 | 1 | elexd 3504 |
. . . . 5
⊢ (𝜑 → 𝐻 ∈ V) |
| 3 | | f1otrkg.p |
. . . . . . . . 9
⊢ 𝑃 = (Base‘𝐺) |
| 4 | | f1otrkg.d |
. . . . . . . . 9
⊢ 𝐷 = (dist‘𝐺) |
| 5 | | f1otrkg.i |
. . . . . . . . 9
⊢ 𝐼 = (Itv‘𝐺) |
| 6 | | f1otrg.g |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ TarskiG) |
| 8 | | f1otrkg.f |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝑃) |
| 9 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵⟶𝑃) |
| 10 | 8, 9 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐵⟶𝑃) |
| 11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃) |
| 12 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
| 13 | 11, 12 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃) |
| 14 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
| 15 | 11, 14 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃) |
| 16 | 3, 4, 5, 7, 13, 15 | axtgcgrrflx 28470 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑦)𝐷(𝐹‘𝑥))) |
| 17 | | f1otrkg.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐻) |
| 18 | | f1otrkg.e |
. . . . . . . . 9
⊢ 𝐸 = (dist‘𝐻) |
| 19 | | f1otrkg.j |
. . . . . . . . 9
⊢ 𝐽 = (Itv‘𝐻) |
| 20 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐹:𝐵–1-1-onto→𝑃) |
| 21 | | f1otrkg.1 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 22 | 21 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 23 | | f1otrkg.2 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 24 | 23 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 25 | 3, 4, 5, 17, 18, 19, 20, 22, 24, 12, 14 | f1otrgds 28877 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦))) |
| 26 | 3, 4, 5, 17, 18, 19, 20, 22, 24, 14, 12 | f1otrgds 28877 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦𝐸𝑥) = ((𝐹‘𝑦)𝐷(𝐹‘𝑥))) |
| 27 | 16, 25, 26 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐸𝑦) = (𝑦𝐸𝑥)) |
| 28 | 27 | ralrimivva 3202 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥)) |
| 29 | | f1of1 6847 |
. . . . . . . . . . 11
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵–1-1→𝑃) |
| 30 | 8, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐵–1-1→𝑃) |
| 31 | 30 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵–1-1→𝑃) |
| 32 | | simp21 1207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 ∈ 𝐵) |
| 33 | | simp22 1208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑦 ∈ 𝐵) |
| 34 | 32, 33 | jca 511 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
| 35 | 6 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐺 ∈ TarskiG) |
| 36 | 10 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵⟶𝑃) |
| 37 | 36, 32 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑥) ∈ 𝑃) |
| 38 | 36, 33 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑦) ∈ 𝑃) |
| 39 | | simp23 1209 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑧 ∈ 𝐵) |
| 40 | 36, 39 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑧) ∈ 𝑃) |
| 41 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) |
| 42 | 8 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝐹:𝐵–1-1-onto→𝑃) |
| 43 | 21 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 44 | 23 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 45 | 3, 4, 5, 17, 18, 19, 42, 43, 44, 32, 33 | f1otrgds 28877 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦))) |
| 46 | 3, 4, 5, 17, 18, 19, 42, 43, 44, 39, 39 | f1otrgds 28877 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝑧𝐸𝑧) = ((𝐹‘𝑧)𝐷(𝐹‘𝑧))) |
| 47 | 41, 45, 46 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑧)𝐷(𝐹‘𝑧))) |
| 48 | 3, 4, 5, 35, 37, 38, 40, 47 | axtgcgrid 28471 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
| 49 | | f1veqaeq 7277 |
. . . . . . . . . 10
⊢ ((𝐹:𝐵–1-1→𝑃 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
| 50 | 49 | imp 406 |
. . . . . . . . 9
⊢ (((𝐹:𝐵–1-1→𝑃 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 = 𝑦) |
| 51 | 31, 34, 48, 50 | syl21anc 838 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑥𝐸𝑦) = (𝑧𝐸𝑧)) → 𝑥 = 𝑦) |
| 52 | 51 | 3expia 1122 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)) |
| 53 | 52 | ralrimivvva 3205 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)) |
| 54 | 28, 53 | jca 511 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦))) |
| 55 | 17, 18, 19 | istrkgc 28462 |
. . . . 5
⊢ (𝐻 ∈ TarskiGC
↔ (𝐻 ∈ V ∧
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐸𝑦) = (𝑦𝐸𝑥) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥𝐸𝑦) = (𝑧𝐸𝑧) → 𝑥 = 𝑦)))) |
| 56 | 2, 54, 55 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 𝐻 ∈
TarskiGC) |
| 57 | 8 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵–1-1-onto→𝑃) |
| 58 | 57, 29 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐹:𝐵–1-1→𝑃) |
| 59 | | simp2 1138 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) |
| 60 | 6 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝐺 ∈ TarskiG) |
| 61 | 13 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑥) ∈ 𝑃) |
| 62 | 15 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑦) ∈ 𝑃) |
| 63 | | simp3 1139 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ (𝑥𝐽𝑥)) |
| 64 | 21 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 65 | 23 | 3ad2antl1 1186 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 66 | 12 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 ∈ 𝐵) |
| 67 | 14 | 3adant3 1133 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑦 ∈ 𝐵) |
| 68 | 3, 4, 5, 17, 18, 19, 57, 64, 65, 66, 66, 67 | f1otrgitv 28878 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝑦 ∈ (𝑥𝐽𝑥) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑥)))) |
| 69 | 63, 68 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑥))) |
| 70 | 3, 4, 5, 60, 61, 62, 69 | axtgbtwnid 28474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
| 71 | 58, 59, 70, 50 | syl21anc 838 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑦 ∈ (𝑥𝐽𝑥)) → 𝑥 = 𝑦) |
| 72 | 71 | 3expia 1122 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦)) |
| 73 | 72 | ralrimivva 3202 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦)) |
| 74 | | f1ocnv 6860 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝐵–1-1-onto→𝑃 → ◡𝐹:𝑃–1-1-onto→𝐵) |
| 75 | | f1of 6848 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹:𝑃–1-1-onto→𝐵 → ◡𝐹:𝑃⟶𝐵) |
| 76 | 8, 74, 75 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ◡𝐹:𝑃⟶𝐵) |
| 77 | 76 | ad5antr 734 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ◡𝐹:𝑃⟶𝐵) |
| 78 | | simplr 769 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ 𝑃) |
| 79 | 77, 78 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (◡𝐹‘𝑐) ∈ 𝐵) |
| 80 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → 𝑎 = (◡𝐹‘𝑐)) |
| 81 | 80 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → (𝑎 ∈ (𝑢𝐽𝑦) ↔ (◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦))) |
| 82 | 80 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → (𝑎 ∈ (𝑣𝐽𝑥) ↔ (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥))) |
| 83 | 81, 82 | anbi12d 632 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ 𝑎 = (◡𝐹‘𝑐)) → ((𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)) ↔ ((◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ∧ (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥)))) |
| 84 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦))) |
| 85 | 20 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵–1-1-onto→𝑃) |
| 86 | 85 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝐹:𝐵–1-1-onto→𝑃) |
| 87 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑐)) = 𝑐) |
| 88 | 87 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ↔ 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))) |
| 89 | 86, 78, 88 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ↔ 𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))) |
| 90 | 84, 89 | mpbird 257 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦))) |
| 91 | 22 | ad4ant14 752 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 92 | 91 | ad4ant14 752 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 93 | 24 | ad4ant14 752 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 94 | 93 | ad4ant14 752 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 95 | | simplr2 1217 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ 𝐵) |
| 96 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑢 ∈ 𝐵) |
| 97 | 14 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑦 ∈ 𝐵) |
| 98 | 97 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑦 ∈ 𝐵) |
| 99 | 3, 4, 5, 17, 18, 19, 86, 92, 94, 96, 98, 79 | f1otrgitv 28878 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)))) |
| 100 | 90, 99 | mpbird 257 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦)) |
| 101 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))) |
| 102 | 87 | eleq1d 2826 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑐 ∈ 𝑃) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)) ↔ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
| 103 | 86, 78, 102 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)) ↔ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
| 104 | 101, 103 | mpbird 257 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥))) |
| 105 | | simplr3 1218 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ 𝐵) |
| 106 | 105 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑣 ∈ 𝐵) |
| 107 | 12 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑥 ∈ 𝐵) |
| 108 | 107 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → 𝑥 ∈ 𝐵) |
| 109 | 3, 4, 5, 17, 18, 19, 86, 92, 94, 106, 108, 79 | f1otrgitv 28878 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
| 110 | 104, 109 | mpbird 257 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥)) |
| 111 | 100, 110 | jca 511 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ((◡𝐹‘𝑐) ∈ (𝑢𝐽𝑦) ∧ (◡𝐹‘𝑐) ∈ (𝑣𝐽𝑥))) |
| 112 | 79, 83, 111 | rspcedvd 3624 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) ∧ 𝑐 ∈ 𝑃) ∧ (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) |
| 113 | 7 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐺 ∈ TarskiG) |
| 114 | 11 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝐹:𝐵⟶𝑃) |
| 115 | 114, 107 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑥) ∈ 𝑃) |
| 116 | 114, 97 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑦) ∈ 𝑃) |
| 117 | | simplr1 1216 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑧 ∈ 𝐵) |
| 118 | 114, 117 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑧) ∈ 𝑃) |
| 119 | 114, 95 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑢) ∈ 𝑃) |
| 120 | 114, 105 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑣) ∈ 𝑃) |
| 121 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑢 ∈ (𝑥𝐽𝑧)) |
| 122 | 3, 4, 5, 17, 18, 19, 85, 91, 93, 107, 117, 95 | f1otrgitv 28878 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑢 ∈ (𝑥𝐽𝑧) ↔ (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧)))) |
| 123 | 121, 122 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑢) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧))) |
| 124 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → 𝑣 ∈ (𝑦𝐽𝑧)) |
| 125 | 3, 4, 5, 17, 18, 19, 85, 91, 93, 97, 117, 105 | f1otrgitv 28878 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝑣 ∈ (𝑦𝐽𝑧) ↔ (𝐹‘𝑣) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧)))) |
| 126 | 124, 125 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → (𝐹‘𝑣) ∈ ((𝐹‘𝑦)𝐼(𝐹‘𝑧))) |
| 127 | 3, 4, 5, 113, 115, 116, 118, 119, 120, 123, 126 | axtgpasch 28475 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑐 ∈ 𝑃 (𝑐 ∈ ((𝐹‘𝑢)𝐼(𝐹‘𝑦)) ∧ 𝑐 ∈ ((𝐹‘𝑣)𝐼(𝐹‘𝑥)))) |
| 128 | 112, 127 | r19.29a 3162 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) ∧ (𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧))) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) |
| 129 | 128 | ex 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑧 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵)) → ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))) |
| 130 | 129 | ralrimivvva 3205 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))) |
| 131 | 130 | ralrimivva 3202 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥)))) |
| 132 | 8 | ad5antr 734 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃) |
| 133 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ 𝑃) |
| 134 | 132, 133,
87 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘(◡𝐹‘𝑐)) = 𝑐) |
| 135 | | ffn 6736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:𝐵⟶𝑃 → 𝐹 Fn 𝐵) |
| 136 | 132, 9, 135 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹 Fn 𝐵) |
| 137 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) |
| 138 | 137 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ∈ 𝒫 𝐵) |
| 139 | 138 | elpwid 4609 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ 𝐵) |
| 140 | 139 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑠 ⊆ 𝐵) |
| 141 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠) |
| 142 | | fnfvima 7253 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn 𝐵 ∧ 𝑠 ⊆ 𝐵 ∧ 𝑥 ∈ 𝑠) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑠)) |
| 143 | 136, 140,
141, 142 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘𝑥) ∈ (𝐹 “ 𝑠)) |
| 144 | 137 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ∈ 𝒫 𝐵) |
| 145 | 144 | elpwid 4609 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ 𝐵) |
| 146 | 145 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑡 ⊆ 𝐵) |
| 147 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡) |
| 148 | | fnfvima 7253 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 Fn 𝐵 ∧ 𝑡 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑡) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑡)) |
| 149 | 136, 146,
147, 148 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘𝑦) ∈ (𝐹 “ 𝑡)) |
| 150 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) |
| 151 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = (𝐹‘𝑥) → (𝑒𝐼𝑓) = ((𝐹‘𝑥)𝐼𝑓)) |
| 152 | 151 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = (𝐹‘𝑥) → (𝑐 ∈ (𝑒𝐼𝑓) ↔ 𝑐 ∈ ((𝐹‘𝑥)𝐼𝑓))) |
| 153 | | oveq2 7439 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐹‘𝑦) → ((𝐹‘𝑥)𝐼𝑓) = ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
| 154 | 153 | eleq2d 2827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐹‘𝑦) → (𝑐 ∈ ((𝐹‘𝑥)𝐼𝑓) ↔ 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))) |
| 155 | 152, 154 | rspc2va 3634 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐹‘𝑥) ∈ (𝐹 “ 𝑠) ∧ (𝐹‘𝑦) ∈ (𝐹 “ 𝑡)) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
| 156 | 143, 149,
150, 155 | syl21anc 838 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
| 157 | 134, 156 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦))) |
| 158 | 8 | ad4antr 732 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃) |
| 159 | | simp-5l 785 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → 𝜑) |
| 160 | 159, 21 | sylancom 588 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 161 | | simp-5l 785 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝜑) |
| 162 | 161, 23 | sylancom 588 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 163 | | simprl 771 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝑠) |
| 164 | 139, 163 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑥 ∈ 𝐵) |
| 165 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝑡) |
| 166 | 145, 165 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑦 ∈ 𝐵) |
| 167 | 76 | ad4antr 732 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ◡𝐹:𝑃⟶𝐵) |
| 168 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → 𝑐 ∈ 𝑃) |
| 169 | 167, 168 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (◡𝐹‘𝑐) ∈ 𝐵) |
| 170 | 3, 4, 5, 17, 18, 19, 158, 160, 162, 164, 166, 169 | f1otrgitv 28878 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ((◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))) |
| 171 | 170 | adantlr 715 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → ((◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) ↔ (𝐹‘(◡𝐹‘𝑐)) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑦)))) |
| 172 | 157, 171 | mpbird 257 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑦 ∈ 𝑡)) → (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)) |
| 173 | 172 | ralrimivva 3202 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)) |
| 174 | 173 | adantllr 719 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦)) |
| 175 | 76 | ad4antr 732 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → ◡𝐹:𝑃⟶𝐵) |
| 176 | | simpr 484 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ 𝑃) |
| 177 | 175, 176 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → (◡𝐹‘𝑐) ∈ 𝐵) |
| 178 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (◡𝐹‘𝑐) → (𝑏 ∈ (𝑥𝐽𝑦) ↔ (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))) |
| 179 | 178 | 2ralbidv 3221 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (◡𝐹‘𝑐) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))) |
| 180 | 179 | adantl 481 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 = (◡𝐹‘𝑐)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦) ↔ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦))) |
| 181 | 177, 180 | rspcedv 3615 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
| 182 | 181 | adantr 480 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → (∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 (◡𝐹‘𝑐) ∈ (𝑥𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
| 183 | 174, 182 | mpd 15 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑐 ∈ 𝑃) ∧ ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)) |
| 184 | 6 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐺 ∈ TarskiG) |
| 185 | | imassrn 6089 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑠) ⊆ ran 𝐹 |
| 186 | | f1ofo 6855 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐵–1-1-onto→𝑃 → 𝐹:𝐵–onto→𝑃) |
| 187 | | forn 6823 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐵–onto→𝑃 → ran 𝐹 = 𝑃) |
| 188 | 8, 186, 187 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝐹 = 𝑃) |
| 189 | 188 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ran 𝐹 = 𝑃) |
| 190 | 185, 189 | sseqtrid 4026 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹 “ 𝑠) ⊆ 𝑃) |
| 191 | | imassrn 6089 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑡) ⊆ ran 𝐹 |
| 192 | 191, 189 | sseqtrid 4026 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹 “ 𝑡) ⊆ 𝑃) |
| 193 | 10 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝐹:𝐵⟶𝑃) |
| 194 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → 𝑎 ∈ 𝐵) |
| 195 | 193, 194 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (𝐹‘𝑎) ∈ 𝑃) |
| 196 | 8 | ad5antr 734 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝐹:𝐵–1-1-onto→𝑃) |
| 197 | | ffn 6736 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹:𝑃⟶𝐵 → ◡𝐹 Fn 𝑃) |
| 198 | 196, 74, 75, 197 | 4syl 19 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ◡𝐹 Fn 𝑃) |
| 199 | 190 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹 “ 𝑠) ⊆ 𝑃) |
| 200 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ (𝐹 “ 𝑠)) |
| 201 | | fnfvima 7253 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐹 Fn 𝑃 ∧ (𝐹 “ 𝑠) ⊆ 𝑃 ∧ 𝑢 ∈ (𝐹 “ 𝑠)) → (◡𝐹‘𝑢) ∈ (◡𝐹 “ (𝐹 “ 𝑠))) |
| 202 | 198, 199,
200, 201 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ (◡𝐹 “ (𝐹 “ 𝑠))) |
| 203 | 196, 29 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝐹:𝐵–1-1→𝑃) |
| 204 | | simp-5r 786 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) |
| 205 | 204 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑠 ∈ 𝒫 𝐵) |
| 206 | 205 | elpwid 4609 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑠 ⊆ 𝐵) |
| 207 | | f1imacnv 6864 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐵–1-1→𝑃 ∧ 𝑠 ⊆ 𝐵) → (◡𝐹 “ (𝐹 “ 𝑠)) = 𝑠) |
| 208 | 203, 206,
207 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹 “ (𝐹 “ 𝑠)) = 𝑠) |
| 209 | 202, 208 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ 𝑠) |
| 210 | 192 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹 “ 𝑡) ⊆ 𝑃) |
| 211 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑣 ∈ (𝐹 “ 𝑡)) |
| 212 | | fnfvima 7253 |
. . . . . . . . . . . . . . . 16
⊢ ((◡𝐹 Fn 𝑃 ∧ (𝐹 “ 𝑡) ⊆ 𝑃 ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ (◡𝐹 “ (𝐹 “ 𝑡))) |
| 213 | 198, 210,
211, 212 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ (◡𝐹 “ (𝐹 “ 𝑡))) |
| 214 | 204 | simprd 495 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑡 ∈ 𝒫 𝐵) |
| 215 | 214 | elpwid 4609 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑡 ⊆ 𝐵) |
| 216 | | f1imacnv 6864 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:𝐵–1-1→𝑃 ∧ 𝑡 ⊆ 𝐵) → (◡𝐹 “ (𝐹 “ 𝑡)) = 𝑡) |
| 217 | 203, 215,
216 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹 “ (𝐹 “ 𝑡)) = 𝑡) |
| 218 | 213, 217 | eleqtrd 2843 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ 𝑡) |
| 219 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) |
| 220 | | eleq1 2829 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (◡𝐹‘𝑢) → (𝑥 ∈ (𝑎𝐽𝑦) ↔ (◡𝐹‘𝑢) ∈ (𝑎𝐽𝑦))) |
| 221 | | oveq2 7439 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (◡𝐹‘𝑣) → (𝑎𝐽𝑦) = (𝑎𝐽(◡𝐹‘𝑣))) |
| 222 | 221 | eleq2d 2827 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (◡𝐹‘𝑣) → ((◡𝐹‘𝑢) ∈ (𝑎𝐽𝑦) ↔ (◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣)))) |
| 223 | 220, 222 | rspc2va 3634 |
. . . . . . . . . . . . . 14
⊢ ((((◡𝐹‘𝑢) ∈ 𝑠 ∧ (◡𝐹‘𝑣) ∈ 𝑡) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → (◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣))) |
| 224 | 209, 218,
219, 223 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣))) |
| 225 | | simp-6l 787 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → 𝜑) |
| 226 | 225, 21 | sylancom 588 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 227 | | simp-6l 787 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → 𝜑) |
| 228 | 227, 23 | sylancom 588 |
. . . . . . . . . . . . . 14
⊢
(((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 229 | | simp-4r 784 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑎 ∈ 𝐵) |
| 230 | 210, 211 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑣 ∈ 𝑃) |
| 231 | | f1ocnvdm 7305 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) → (◡𝐹‘𝑣) ∈ 𝐵) |
| 232 | 196, 230,
231 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑣) ∈ 𝐵) |
| 233 | 199, 200 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ 𝑃) |
| 234 | | f1ocnvdm 7305 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑢 ∈ 𝑃) → (◡𝐹‘𝑢) ∈ 𝐵) |
| 235 | 196, 233,
234 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (◡𝐹‘𝑢) ∈ 𝐵) |
| 236 | 3, 4, 5, 17, 18, 19, 196, 226, 228, 229, 232, 235 | f1otrgitv 28878 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ((◡𝐹‘𝑢) ∈ (𝑎𝐽(◡𝐹‘𝑣)) ↔ (𝐹‘(◡𝐹‘𝑢)) ∈ ((𝐹‘𝑎)𝐼(𝐹‘(◡𝐹‘𝑣))))) |
| 237 | 224, 236 | mpbid 232 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(◡𝐹‘𝑢)) ∈ ((𝐹‘𝑎)𝐼(𝐹‘(◡𝐹‘𝑣)))) |
| 238 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑢 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑢)) = 𝑢) |
| 239 | 196, 233,
238 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(◡𝐹‘𝑢)) = 𝑢) |
| 240 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑣 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑣)) = 𝑣) |
| 241 | 196, 230,
240 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → (𝐹‘(◡𝐹‘𝑣)) = 𝑣) |
| 242 | 241 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → ((𝐹‘𝑎)𝐼(𝐹‘(◡𝐹‘𝑣))) = ((𝐹‘𝑎)𝐼𝑣)) |
| 243 | 237, 239,
242 | 3eltr3d 2855 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠)) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ ((𝐹‘𝑎)𝐼𝑣)) |
| 244 | 243 | 3impa 1110 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) ∧ 𝑢 ∈ (𝐹 “ 𝑠) ∧ 𝑣 ∈ (𝐹 “ 𝑡)) → 𝑢 ∈ ((𝐹‘𝑎)𝐼𝑣)) |
| 245 | 3, 4, 5, 184, 190, 192, 195, 244 | axtgcont 28477 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑐 ∈ 𝑃 ∀𝑒 ∈ (𝐹 “ 𝑠)∀𝑓 ∈ (𝐹 “ 𝑡)𝑐 ∈ (𝑒𝐼𝑓)) |
| 246 | 183, 245 | r19.29a 3162 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) ∧ 𝑎 ∈ 𝐵) ∧ ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦)) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)) |
| 247 | 246 | rexlimdva2 3157 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
| 248 | 247 | ralrimivva 3202 |
. . . . . 6
⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))) |
| 249 | 73, 131, 248 | 3jca 1129 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦)))) |
| 250 | 17, 18, 19 | istrkgb 28463 |
. . . . 5
⊢ (𝐻 ∈ TarskiGB
↔ (𝐻 ∈ V ∧
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ((𝑢 ∈ (𝑥𝐽𝑧) ∧ 𝑣 ∈ (𝑦𝐽𝑧)) → ∃𝑎 ∈ 𝐵 (𝑎 ∈ (𝑢𝐽𝑦) ∧ 𝑎 ∈ (𝑣𝐽𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(∃𝑎 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑥 ∈ (𝑎𝐽𝑦) → ∃𝑏 ∈ 𝐵 ∀𝑥 ∈ 𝑠 ∀𝑦 ∈ 𝑡 𝑏 ∈ (𝑥𝐽𝑦))))) |
| 251 | 2, 249, 250 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 𝐻 ∈
TarskiGB) |
| 252 | 56, 251 | elind 4200 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (TarskiGC ∩
TarskiGB)) |
| 253 | 6 | ad9antr 742 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐺 ∈ TarskiG) |
| 254 | 10 | ad9antr 742 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵⟶𝑃) |
| 255 | | simp-9r 794 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥 ∈ 𝐵) |
| 256 | 254, 255 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑥) ∈ 𝑃) |
| 257 | | simp-8r 792 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ 𝐵) |
| 258 | 254, 257 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑦) ∈ 𝑃) |
| 259 | | simp-7r 790 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑧 ∈ 𝐵) |
| 260 | 254, 259 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑧) ∈ 𝑃) |
| 261 | | simp-5r 786 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑎 ∈ 𝐵) |
| 262 | 254, 261 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑎) ∈ 𝑃) |
| 263 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ 𝐵) |
| 264 | 254, 263 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑏) ∈ 𝑃) |
| 265 | | simpllr 776 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑐 ∈ 𝐵) |
| 266 | 254, 265 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑐) ∈ 𝑃) |
| 267 | | simp-6r 788 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑢 ∈ 𝐵) |
| 268 | 254, 267 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑢) ∈ 𝑃) |
| 269 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑣 ∈ 𝐵) |
| 270 | 254, 269 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑣) ∈ 𝑃) |
| 271 | 8 | ad9antr 742 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝐹:𝐵–1-1-onto→𝑃) |
| 272 | 271, 255 | jca 511 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵)) |
| 273 | | simprl1 1219 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑥 ≠ 𝑦) |
| 274 | | dff1o6 7295 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝐵–1-1-onto→𝑃 ↔ (𝐹 Fn 𝐵 ∧ ran 𝐹 = 𝑃 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))) |
| 275 | 274 | simp3bi 1148 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝐵–1-1-onto→𝑃 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
| 276 | 275 | r19.21bi 3251 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
| 277 | 276 | r19.21bi 3251 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) |
| 278 | 277 | necon3d 2961 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → (𝑥 ≠ 𝑦 → (𝐹‘𝑥) ≠ (𝐹‘𝑦))) |
| 279 | 278 | imp 406 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ≠ 𝑦) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
| 280 | 272, 257,
273, 279 | syl21anc 838 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑥) ≠ (𝐹‘𝑦)) |
| 281 | | simprl2 1220 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑦 ∈ (𝑥𝐽𝑧)) |
| 282 | 21 | ex 412 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))) |
| 283 | 282 | ad9antr 742 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓)))) |
| 284 | 283 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 285 | 23 | ex 412 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))) |
| 286 | 285 | ad9antr 742 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))))) |
| 287 | 286 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 288 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 255, 259, 257 | f1otrgitv 28878 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧)))) |
| 289 | 281, 288 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘𝑧))) |
| 290 | | simprl3 1221 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → 𝑏 ∈ (𝑎𝐽𝑐)) |
| 291 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 261, 265, 263 | f1otrgitv 28878 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏 ∈ (𝑎𝐽𝑐) ↔ (𝐹‘𝑏) ∈ ((𝐹‘𝑎)𝐼(𝐹‘𝑐)))) |
| 292 | 290, 291 | mpbid 232 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝐹‘𝑏) ∈ ((𝐹‘𝑎)𝐼(𝐹‘𝑐))) |
| 293 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) |
| 294 | 293 | simpld 494 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐))) |
| 295 | 294 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = (𝑎𝐸𝑏)) |
| 296 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 255, 257 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑦) = ((𝐹‘𝑥)𝐷(𝐹‘𝑦))) |
| 297 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 261, 263 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑏) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
| 298 | 295, 296,
297 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑥)𝐷(𝐹‘𝑦)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
| 299 | 294 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) |
| 300 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 257, 259 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑧) = ((𝐹‘𝑦)𝐷(𝐹‘𝑧))) |
| 301 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 263, 265 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑐) = ((𝐹‘𝑏)𝐷(𝐹‘𝑐))) |
| 302 | 299, 300,
301 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑦)𝐷(𝐹‘𝑧)) = ((𝐹‘𝑏)𝐷(𝐹‘𝑐))) |
| 303 | 293 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))) |
| 304 | 303 | simpld 494 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = (𝑎𝐸𝑣)) |
| 305 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 255, 267 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑥𝐸𝑢) = ((𝐹‘𝑥)𝐷(𝐹‘𝑢))) |
| 306 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 261, 269 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑎𝐸𝑣) = ((𝐹‘𝑎)𝐷(𝐹‘𝑣))) |
| 307 | 304, 305,
306 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑥)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑣))) |
| 308 | 303 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = (𝑏𝐸𝑣)) |
| 309 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 257, 267 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑦𝐸𝑢) = ((𝐹‘𝑦)𝐷(𝐹‘𝑢))) |
| 310 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 263, 269 | f1otrgds 28877 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑏𝐸𝑣) = ((𝐹‘𝑏)𝐷(𝐹‘𝑣))) |
| 311 | 308, 309,
310 | 3eqtr3d 2785 |
. . . . . . . . . . . . . . . . 17
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑦)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑏)𝐷(𝐹‘𝑣))) |
| 312 | 3, 4, 5, 253, 256, 258, 260, 262, 264, 266, 268, 270, 280, 289, 292, 298, 302, 307, 311 | axtg5seg 28473 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → ((𝐹‘𝑧)𝐷(𝐹‘𝑢)) = ((𝐹‘𝑐)𝐷(𝐹‘𝑣))) |
| 313 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 259, 267 | f1otrgds 28877 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = ((𝐹‘𝑧)𝐷(𝐹‘𝑢))) |
| 314 | 3, 4, 5, 17, 18, 19, 271, 284, 287, 265, 269 | f1otrgds 28877 |
. . . . . . . . . . . . . . . 16
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑐𝐸𝑣) = ((𝐹‘𝑐)𝐷(𝐹‘𝑣))) |
| 315 | 312, 313,
314 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . 15
⊢
((((((((((𝜑 ∧
𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) ∧ ((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣))))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) |
| 316 | 315 | ex 412 |
. . . . . . . . . . . . . 14
⊢
(((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ 𝑣 ∈ 𝐵) → (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 317 | 316 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢
((((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 318 | 317 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐵) → ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 319 | 318 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) ∧ 𝑎 ∈ 𝐵) → ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 320 | 319 | ralrimiva 3146 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) ∧ 𝑢 ∈ 𝐵) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 321 | 320 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 322 | 321 | ralrimiva 3146 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 323 | 322 | ralrimiva 3146 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 324 | 323 | ralrimiva 3146 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣))) |
| 325 | | simp-4l 783 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝜑) |
| 326 | | simplr 769 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑤 ∈ 𝑃) |
| 327 | | simprl 771 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤)) |
| 328 | 325, 8 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝐹:𝐵–1-1-onto→𝑃) |
| 329 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐵–1-1-onto→𝑃 ∧ 𝑤 ∈ 𝑃) → (𝐹‘(◡𝐹‘𝑤)) = 𝑤) |
| 330 | 328, 326,
329 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘(◡𝐹‘𝑤)) = 𝑤) |
| 331 | 330 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑤))) = ((𝐹‘𝑥)𝐼𝑤)) |
| 332 | 327, 331 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑤)))) |
| 333 | 325, 21 | sylan 580 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑒𝐸𝑓) = ((𝐹‘𝑒)𝐷(𝐹‘𝑓))) |
| 334 | 325, 23 | sylan 580 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
| 335 | 12 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑥 ∈ 𝐵) |
| 336 | 76 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑃) → (◡𝐹‘𝑤) ∈ 𝐵) |
| 337 | 325, 326,
336 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (◡𝐹‘𝑤) ∈ 𝐵) |
| 338 | 14 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑦 ∈ 𝐵) |
| 339 | 3, 4, 5, 17, 18, 19, 328, 333, 334, 335, 337, 338 | f1otrgitv 28878 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ↔ (𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼(𝐹‘(◡𝐹‘𝑤))))) |
| 340 | 332, 339 | mpbird 257 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤))) |
| 341 | 3, 4, 5, 17, 18, 19, 328, 333, 334, 338, 337 | f1otrgds 28877 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(◡𝐹‘𝑤)) = ((𝐹‘𝑦)𝐷(𝐹‘(◡𝐹‘𝑤)))) |
| 342 | 330 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑦)𝐷(𝐹‘(◡𝐹‘𝑤))) = ((𝐹‘𝑦)𝐷𝑤)) |
| 343 | | simprr 773 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
| 344 | 341, 342,
343 | 3eqtrd 2781 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(◡𝐹‘𝑤)) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
| 345 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
| 346 | 345 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑎 ∈ 𝐵) |
| 347 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
| 348 | 347 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → 𝑏 ∈ 𝐵) |
| 349 | 3, 4, 5, 17, 18, 19, 328, 333, 334, 346, 348 | f1otrgds 28877 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑎𝐸𝑏) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏))) |
| 350 | 344, 349 | eqtr4d 2780 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)) |
| 351 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (◡𝐹‘𝑤) → (𝑥𝐽𝑧) = (𝑥𝐽(◡𝐹‘𝑤))) |
| 352 | 351 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (◡𝐹‘𝑤) → (𝑦 ∈ (𝑥𝐽𝑧) ↔ 𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)))) |
| 353 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (◡𝐹‘𝑤) → (𝑦𝐸𝑧) = (𝑦𝐸(◡𝐹‘𝑤))) |
| 354 | 353 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (◡𝐹‘𝑤) → ((𝑦𝐸𝑧) = (𝑎𝐸𝑏) ↔ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏))) |
| 355 | 352, 354 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (◡𝐹‘𝑤) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)))) |
| 356 | 355 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑃) ∧ 𝑧 = (◡𝐹‘𝑤)) → ((𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)) ↔ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)))) |
| 357 | 336, 356 | rspcedv 3615 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑃) → ((𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏)) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏)))) |
| 358 | 357 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑃) ∧ (𝑦 ∈ (𝑥𝐽(◡𝐹‘𝑤)) ∧ (𝑦𝐸(◡𝐹‘𝑤)) = (𝑎𝐸𝑏))) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
| 359 | 325, 326,
340, 350, 358 | syl22anc 839 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ 𝑤 ∈ 𝑃) ∧ ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
| 360 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐺 ∈ TarskiG) |
| 361 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑥) ∈ 𝑃) |
| 362 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑦) ∈ 𝑃) |
| 363 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝐹:𝐵⟶𝑃) |
| 364 | 363, 345 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑎) ∈ 𝑃) |
| 365 | 363, 347 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝐹‘𝑏) ∈ 𝑃) |
| 366 | 3, 4, 5, 360, 361, 362, 364, 365 | axtgsegcon 28472 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑤 ∈ 𝑃 ((𝐹‘𝑦) ∈ ((𝐹‘𝑥)𝐼𝑤) ∧ ((𝐹‘𝑦)𝐷𝑤) = ((𝐹‘𝑎)𝐷(𝐹‘𝑏)))) |
| 367 | 359, 366 | r19.29a 3162 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
| 368 | 367 | ralrimivva 3202 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
| 369 | 368 | ralrimivva 3202 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))) |
| 370 | 2, 324, 369 | jca32 515 |
. . . . 5
⊢ (𝜑 → (𝐻 ∈ V ∧ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))) |
| 371 | 17, 18, 19 | istrkgcb 28464 |
. . . . 5
⊢ (𝐻 ∈ TarskiGCB
↔ (𝐻 ∈ V ∧
(∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 ∀𝑣 ∈ 𝐵 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐽𝑧) ∧ 𝑏 ∈ (𝑎𝐽𝑐)) ∧ (((𝑥𝐸𝑦) = (𝑎𝐸𝑏) ∧ (𝑦𝐸𝑧) = (𝑏𝐸𝑐)) ∧ ((𝑥𝐸𝑢) = (𝑎𝐸𝑣) ∧ (𝑦𝐸𝑢) = (𝑏𝐸𝑣)))) → (𝑧𝐸𝑢) = (𝑐𝐸𝑣)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (𝑦 ∈ (𝑥𝐽𝑧) ∧ (𝑦𝐸𝑧) = (𝑎𝐸𝑏))))) |
| 372 | 370, 371 | sylibr 234 |
. . . 4
⊢ (𝜑 → 𝐻 ∈
TarskiGCB) |
| 373 | | f1otrg.l |
. . . . 5
⊢ (𝜑 → (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))})) |
| 374 | 17, 18, 19 | istrkgl 28466 |
. . . . 5
⊢ (𝐻 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})} ↔ (𝐻 ∈ V ∧ (LineG‘𝐻) = (𝑥 ∈ 𝐵, 𝑦 ∈ (𝐵 ∖ {𝑥}) ↦ {𝑧 ∈ 𝐵 ∣ (𝑧 ∈ (𝑥𝐽𝑦) ∨ 𝑥 ∈ (𝑧𝐽𝑦) ∨ 𝑦 ∈ (𝑥𝐽𝑧))}))) |
| 375 | 2, 373, 374 | sylanbrc 583 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) |
| 376 | 372, 375 | elind 4200 |
. . 3
⊢ (𝜑 → 𝐻 ∈ (TarskiGCB ∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
| 377 | 252, 376 | elind 4200 |
. 2
⊢ (𝜑 → 𝐻 ∈ ((TarskiGC ∩
TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))) |
| 378 | | df-trkg 28461 |
. 2
⊢ TarskiG =
((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB
∩ {𝑓 ∣
[(Base‘𝑓) /
𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) |
| 379 | 377, 378 | eleqtrrdi 2852 |
1
⊢ (𝜑 → 𝐻 ∈ TarskiG) |