Step | Hyp | Ref
| Expression |
1 | | chpg 28008 |
. 2
class
hpG |
2 | | vg |
. . 3
setvar π |
3 | | cvv 3475 |
. . 3
class
V |
4 | | vd |
. . . 4
setvar π |
5 | 2 | cv 1541 |
. . . . . 6
class π |
6 | | clng 27685 |
. . . . . 6
class
LineG |
7 | 5, 6 | cfv 6544 |
. . . . 5
class
(LineGβπ) |
8 | 7 | crn 5678 |
. . . 4
class ran
(LineGβπ) |
9 | | va |
. . . . . . . . . . . . 13
setvar π |
10 | 9 | cv 1541 |
. . . . . . . . . . . 12
class π |
11 | | vp |
. . . . . . . . . . . . . 14
setvar π |
12 | 11 | cv 1541 |
. . . . . . . . . . . . 13
class π |
13 | 4 | cv 1541 |
. . . . . . . . . . . . 13
class π |
14 | 12, 13 | cdif 3946 |
. . . . . . . . . . . 12
class (π β π) |
15 | 10, 14 | wcel 2107 |
. . . . . . . . . . 11
wff π β (π β π) |
16 | | vc |
. . . . . . . . . . . . 13
setvar π |
17 | 16 | cv 1541 |
. . . . . . . . . . . 12
class π |
18 | 17, 14 | wcel 2107 |
. . . . . . . . . . 11
wff π β (π β π) |
19 | 15, 18 | wa 397 |
. . . . . . . . . 10
wff (π β (π β π) β§ π β (π β π)) |
20 | | vt |
. . . . . . . . . . . . 13
setvar π‘ |
21 | 20 | cv 1541 |
. . . . . . . . . . . 12
class π‘ |
22 | | vi |
. . . . . . . . . . . . . 14
setvar π |
23 | 22 | cv 1541 |
. . . . . . . . . . . . 13
class π |
24 | 10, 17, 23 | co 7409 |
. . . . . . . . . . . 12
class (πππ) |
25 | 21, 24 | wcel 2107 |
. . . . . . . . . . 11
wff π‘ β (πππ) |
26 | 25, 20, 13 | wrex 3071 |
. . . . . . . . . 10
wff
βπ‘ β
π π‘ β (πππ) |
27 | 19, 26 | wa 397 |
. . . . . . . . 9
wff ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) |
28 | | vb |
. . . . . . . . . . . . 13
setvar π |
29 | 28 | cv 1541 |
. . . . . . . . . . . 12
class π |
30 | 29, 14 | wcel 2107 |
. . . . . . . . . . 11
wff π β (π β π) |
31 | 30, 18 | wa 397 |
. . . . . . . . . 10
wff (π β (π β π) β§ π β (π β π)) |
32 | 29, 17, 23 | co 7409 |
. . . . . . . . . . . 12
class (πππ) |
33 | 21, 32 | wcel 2107 |
. . . . . . . . . . 11
wff π‘ β (πππ) |
34 | 33, 20, 13 | wrex 3071 |
. . . . . . . . . 10
wff
βπ‘ β
π π‘ β (πππ) |
35 | 31, 34 | wa 397 |
. . . . . . . . 9
wff ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) |
36 | 27, 35 | wa 397 |
. . . . . . . 8
wff (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ))) |
37 | 36, 16, 12 | wrex 3071 |
. . . . . . 7
wff
βπ β
π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ))) |
38 | | citv 27684 |
. . . . . . . 8
class
Itv |
39 | 5, 38 | cfv 6544 |
. . . . . . 7
class
(Itvβπ) |
40 | 37, 22, 39 | wsbc 3778 |
. . . . . 6
wff
[(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ))) |
41 | | cbs 17144 |
. . . . . . 7
class
Base |
42 | 5, 41 | cfv 6544 |
. . . . . 6
class
(Baseβπ) |
43 | 40, 11, 42 | wsbc 3778 |
. . . . 5
wff
[(Baseβπ) / π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ))) |
44 | 43, 9, 28 | copab 5211 |
. . . 4
class
{β¨π, πβ© β£
[(Baseβπ) /
π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)))} |
45 | 4, 8, 44 | cmpt 5232 |
. . 3
class (π β ran (LineGβπ) β¦ {β¨π, πβ© β£ [(Baseβπ) / π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)))}) |
46 | 2, 3, 45 | cmpt 5232 |
. 2
class (π β V β¦ (π β ran (LineGβπ) β¦ {β¨π, πβ© β£ [(Baseβπ) / π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)))})) |
47 | 1, 46 | wceq 1542 |
1
wff hpG =
(π β V β¦ (π β ran (LineGβπ) β¦ {β¨π, πβ© β£ [(Baseβπ) / π][(Itvβπ) / π]βπ β π (((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)) β§ ((π β (π β π) β§ π β (π β π)) β§ βπ‘ β π π‘ β (πππ)))})) |