Step |
Hyp |
Ref |
Expression |
0 |
|
chpg |
⊢ hpG |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
cvv |
⊢ V |
3 |
|
vd |
⊢ 𝑑 |
4 |
|
clng |
⊢ LineG |
5 |
1
|
cv |
⊢ 𝑔 |
6 |
5 4
|
cfv |
⊢ ( LineG ‘ 𝑔 ) |
7 |
6
|
crn |
⊢ ran ( LineG ‘ 𝑔 ) |
8 |
|
va |
⊢ 𝑎 |
9 |
|
vb |
⊢ 𝑏 |
10 |
|
cbs |
⊢ Base |
11 |
5 10
|
cfv |
⊢ ( Base ‘ 𝑔 ) |
12 |
|
vp |
⊢ 𝑝 |
13 |
|
citv |
⊢ Itv |
14 |
5 13
|
cfv |
⊢ ( Itv ‘ 𝑔 ) |
15 |
|
vi |
⊢ 𝑖 |
16 |
|
vc |
⊢ 𝑐 |
17 |
12
|
cv |
⊢ 𝑝 |
18 |
8
|
cv |
⊢ 𝑎 |
19 |
3
|
cv |
⊢ 𝑑 |
20 |
17 19
|
cdif |
⊢ ( 𝑝 ∖ 𝑑 ) |
21 |
18 20
|
wcel |
⊢ 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) |
22 |
16
|
cv |
⊢ 𝑐 |
23 |
22 20
|
wcel |
⊢ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) |
24 |
21 23
|
wa |
⊢ ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) |
25 |
|
vt |
⊢ 𝑡 |
26 |
25
|
cv |
⊢ 𝑡 |
27 |
15
|
cv |
⊢ 𝑖 |
28 |
18 22 27
|
co |
⊢ ( 𝑎 𝑖 𝑐 ) |
29 |
26 28
|
wcel |
⊢ 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) |
30 |
29 25 19
|
wrex |
⊢ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) |
31 |
24 30
|
wa |
⊢ ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) |
32 |
9
|
cv |
⊢ 𝑏 |
33 |
32 20
|
wcel |
⊢ 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) |
34 |
33 23
|
wa |
⊢ ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) |
35 |
32 22 27
|
co |
⊢ ( 𝑏 𝑖 𝑐 ) |
36 |
26 35
|
wcel |
⊢ 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) |
37 |
36 25 19
|
wrex |
⊢ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) |
38 |
34 37
|
wa |
⊢ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) |
39 |
31 38
|
wa |
⊢ ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) |
40 |
39 16 17
|
wrex |
⊢ ∃ 𝑐 ∈ 𝑝 ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) |
41 |
40 15 14
|
wsbc |
⊢ [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑐 ∈ 𝑝 ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) |
42 |
41 12 11
|
wsbc |
⊢ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑐 ∈ 𝑝 ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) |
43 |
42 8 9
|
copab |
⊢ { 〈 𝑎 , 𝑏 〉 ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑐 ∈ 𝑝 ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } |
44 |
3 7 43
|
cmpt |
⊢ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { 〈 𝑎 , 𝑏 〉 ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑐 ∈ 𝑝 ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) |
45 |
1 2 44
|
cmpt |
⊢ ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { 〈 𝑎 , 𝑏 〉 ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑐 ∈ 𝑝 ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) ) |
46 |
0 45
|
wceq |
⊢ hpG = ( 𝑔 ∈ V ↦ ( 𝑑 ∈ ran ( LineG ‘ 𝑔 ) ↦ { 〈 𝑎 , 𝑏 〉 ∣ [ ( Base ‘ 𝑔 ) / 𝑝 ] [ ( Itv ‘ 𝑔 ) / 𝑖 ] ∃ 𝑐 ∈ 𝑝 ( ( ( 𝑎 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑎 𝑖 𝑐 ) ) ∧ ( ( 𝑏 ∈ ( 𝑝 ∖ 𝑑 ) ∧ 𝑐 ∈ ( 𝑝 ∖ 𝑑 ) ) ∧ ∃ 𝑡 ∈ 𝑑 𝑡 ∈ ( 𝑏 𝑖 𝑐 ) ) ) } ) ) |