Step |
Hyp |
Ref |
Expression |
1 |
|
isleag.p |
|- P = ( Base ` G ) |
2 |
|
isleag.g |
|- ( ph -> G e. TarskiG ) |
3 |
|
isleag.a |
|- ( ph -> A e. P ) |
4 |
|
isleag.b |
|- ( ph -> B e. P ) |
5 |
|
isleag.c |
|- ( ph -> C e. P ) |
6 |
|
isleag.d |
|- ( ph -> D e. P ) |
7 |
|
isleag.e |
|- ( ph -> E e. P ) |
8 |
|
isleag.f |
|- ( ph -> F e. P ) |
9 |
|
leagne.1 |
|- ( ph -> <" A B C "> ( leA ` G ) <" D E F "> ) |
10 |
|
eqid |
|- ( Itv ` G ) = ( Itv ` G ) |
11 |
|
eqid |
|- ( hlG ` G ) = ( hlG ` G ) |
12 |
2
|
ad2antrr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> G e. TarskiG ) |
13 |
3
|
ad2antrr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> A e. P ) |
14 |
4
|
ad2antrr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> B e. P ) |
15 |
5
|
ad2antrr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> C e. P ) |
16 |
6
|
ad2antrr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> D e. P ) |
17 |
7
|
ad2antrr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> E e. P ) |
18 |
|
simplr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> x e. P ) |
19 |
|
simprr |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> <" A B C "> ( cgrA ` G ) <" D E x "> ) |
20 |
1 10 11 12 13 14 15 16 17 18 19
|
cgrane1 |
|- ( ( ( ph /\ x e. P ) /\ ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) -> A =/= B ) |
21 |
1 2 3 4 5 6 7 8
|
isleag |
|- ( ph -> ( <" A B C "> ( leA ` G ) <" D E F "> <-> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) ) |
22 |
9 21
|
mpbid |
|- ( ph -> E. x e. P ( x ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E x "> ) ) |
23 |
20 22
|
r19.29a |
|- ( ph -> A =/= B ) |