Step |
Hyp |
Ref |
Expression |
1 |
|
tglineelsb2.p |
|- B = ( Base ` G ) |
2 |
|
tglineelsb2.i |
|- I = ( Itv ` G ) |
3 |
|
tglineelsb2.l |
|- L = ( LineG ` G ) |
4 |
|
tglineelsb2.g |
|- ( ph -> G e. TarskiG ) |
5 |
|
tglineelsb2.1 |
|- ( ph -> P e. B ) |
6 |
|
tglineelsb2.2 |
|- ( ph -> Q e. B ) |
7 |
|
tglineelsb2.4 |
|- ( ph -> P =/= Q ) |
8 |
4
|
3ad2ant1 |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> G e. TarskiG ) |
9 |
5
|
3ad2ant1 |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P e. B ) |
10 |
6
|
3ad2ant1 |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> Q e. B ) |
11 |
7
|
3ad2ant1 |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P =/= Q ) |
12 |
|
simp2l |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> x e. ran L ) |
13 |
|
simp3ll |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P e. x ) |
14 |
|
simp3lr |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> Q e. x ) |
15 |
1 2 3 8 9 10 11 11 12 13 14
|
tglinethru |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> x = ( P L Q ) ) |
16 |
|
simp2r |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> y e. ran L ) |
17 |
|
simp3rl |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> P e. y ) |
18 |
|
simp3rr |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> Q e. y ) |
19 |
1 2 3 8 9 10 11 11 16 17 18
|
tglinethru |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> y = ( P L Q ) ) |
20 |
15 19
|
eqtr4d |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) /\ ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) ) -> x = y ) |
21 |
20
|
3expia |
|- ( ( ph /\ ( x e. ran L /\ y e. ran L ) ) -> ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) ) |
22 |
21
|
ralrimivva |
|- ( ph -> A. x e. ran L A. y e. ran L ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) ) |
23 |
|
eleq2w |
|- ( x = y -> ( P e. x <-> P e. y ) ) |
24 |
|
eleq2w |
|- ( x = y -> ( Q e. x <-> Q e. y ) ) |
25 |
23 24
|
anbi12d |
|- ( x = y -> ( ( P e. x /\ Q e. x ) <-> ( P e. y /\ Q e. y ) ) ) |
26 |
25
|
rmo4 |
|- ( E* x e. ran L ( P e. x /\ Q e. x ) <-> A. x e. ran L A. y e. ran L ( ( ( P e. x /\ Q e. x ) /\ ( P e. y /\ Q e. y ) ) -> x = y ) ) |
27 |
22 26
|
sylibr |
|- ( ph -> E* x e. ran L ( P e. x /\ Q e. x ) ) |