Metamath Proof Explorer

Theorem prlngmolem1

Description: Lemma for prlngmo : Contradiction: Assuming two different parallels B and C having a common point X exist to a line A , the geometry cannot be Euclidean (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses prlngeu.p 
|- P = ( Base ` G )
prlngeu.l 
|- L = ( LineG ` G )
prlngeu.r 
|- .|| = ( parlnG ` G )
prlngeu.g 
|- ( ph -> G e. TarskiG )
prlngeu.a 
|- ( ph -> A e. ran L )
prlngeu.x 
|- ( ph -> X e. ( P \ A ) )
prlngmolem1.o 
|- O = { <. a , b >. | ( ( a e. ( P \ B ) /\ b e. ( P \ B ) ) /\ E. y e. B y e. ( a I b ) ) }
prlngmolem1.q 
|- Q = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. w e. A w e. ( a I b ) ) }
prlngmolem1.i 
|- I = ( Itv ` G )
prlngmolem1.b 
|- ( ph -> B e. ran L )
prlngmolem1.c 
|- ( ph -> C e. ran L )
prlngmolem1.1 
|- ( ph -> A .|| B )
prlngmolem1.2 
|- ( ph -> A .|| C )
prlngmolem1.3 
|- ( ph -> X e. B )
prlngmolem1.4 
|- ( ph -> X e. C )
prlngmolem1.t 
|- ( ph -> T e. A )
prlngmolem1.w 
|- ( ph -> W e. ( C \ B ) )
prlngmolem1.5 
|- ( ph -> B =/= C )
prlngmolem1.6 
|- ( ph -> W O T )
Assertion prlngmolem1 
|- ( ph -> -. G e. TarskiGE )

Proof

Step Hyp Ref Expression
1 prlngeu.p 
 |-  P = ( Base ` G )
2 prlngeu.l 
 |-  L = ( LineG ` G )
3 prlngeu.r 
 |-  .|| = ( parlnG ` G )
4 prlngeu.g 
 |-  ( ph -> G e. TarskiG )
5 prlngeu.a 
 |-  ( ph -> A e. ran L )
6 prlngeu.x 
 |-  ( ph -> X e. ( P \ A ) )
7 prlngmolem1.o 
 |-  O = { <. a , b >. | ( ( a e. ( P \ B ) /\ b e. ( P \ B ) ) /\ E. y e. B y e. ( a I b ) ) }
8 prlngmolem1.q 
 |-  Q = { <. a , b >. | ( ( a e. ( P \ A ) /\ b e. ( P \ A ) ) /\ E. w e. A w e. ( a I b ) ) }
9 prlngmolem1.i 
 |-  I = ( Itv ` G )
10 prlngmolem1.b 
 |-  ( ph -> B e. ran L )
11 prlngmolem1.c 
 |-  ( ph -> C e. ran L )
12 prlngmolem1.1 
 |-  ( ph -> A .|| B )
13 prlngmolem1.2 
 |-  ( ph -> A .|| C )
14 prlngmolem1.3 
 |-  ( ph -> X e. B )
15 prlngmolem1.4 
 |-  ( ph -> X e. C )
16 prlngmolem1.t 
 |-  ( ph -> T e. A )
17 prlngmolem1.w 
 |-  ( ph -> W e. ( C \ B ) )
18 prlngmolem1.5 
 |-  ( ph -> B =/= C )
19 prlngmolem1.6 
 |-  ( ph -> W O T )
20 4 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> G e. TarskiG )
21 20 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> G e. TarskiG )
22 21 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> G e. TarskiG )
23 5 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> A e. ran L )
24 23 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> A e. ran L )
25 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> r e. P )
26 6 eldifad 
 |-  ( ph -> X e. P )
27 26 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> X e. P )
28 27 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> X e. P )
29 28 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> X e. P )
30 eqid 
 |-  ( PlnG ` G ) = ( PlnG ` G )
31 12 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> A .|| B )
32 31 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> A .|| B )
33 6 eldifbd 
 |-  ( ph -> -. X e. A )
34 nelne1 
 |-  ( ( X e. B /\ -. X e. A ) -> B =/= A )
35 14 33 34 syl2anc 
 |-  ( ph -> B =/= A )
36 35 necomd 
 |-  ( ph -> A =/= B )
37 36 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> A =/= B )
38 37 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> A =/= B )
39 10 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> B e. ran L )
40 simp-5r 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> y e. B )
41 1 2 9 20 39 40 tglnpt 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> y e. P )
42 41 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> y e. P )
43 42 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> y e. P )
44 nelne1 
 |-  ( ( X e. C /\ -. X e. A ) -> C =/= A )
45 15 33 44 syl2anc 
 |-  ( ph -> C =/= A )
46 45 necomd 
 |-  ( ph -> A =/= C )
47 2 3 4 13 46 prlngin0 
 |-  ( ph -> ( A i^i C ) = (/) )
48 47 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> ( A i^i C ) = (/) )
49 16 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> T e. A )
50 21 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> G e. TarskiG )
51 17 eldifad 
 |-  ( ph -> W e. C )
52 1 2 9 4 11 51 tglnpt 
 |-  ( ph -> W e. P )
53 52 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> W e. P )
54 53 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> W e. P )
55 28 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> X e. P )
56 1 2 9 4 5 16 tglnpt 
 |-  ( ph -> T e. P )
57 56 ad5antr 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> T e. P )
58 57 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> T e. P )
59 17 eldifbd 
 |-  ( ph -> -. W e. B )
60 nelne2 
 |-  ( ( X e. B /\ -. W e. B ) -> X =/= W )
61 14 59 60 syl2anc 
 |-  ( ph -> X =/= W )
62 61 necomd 
 |-  ( ph -> W =/= X )
63 62 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> W =/= X )
64 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> X = y )
65 simp-4r 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> y e. ( W I T ) )
66 65 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> y e. ( W I T ) )
67 64 66 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> X e. ( W I T ) )
68 1 9 2 50 54 55 58 63 67 btwnlng3 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> T e. ( W L X ) )
69 1 9 2 4 52 26 62 62 11 51 15 tglinethru 
 |-  ( ph -> C = ( W L X ) )
70 69 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> C = ( W L X ) )
71 68 70 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> T e. C )
72 49 71 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> T e. ( A i^i C ) )
73 72 ne0d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> ( A i^i C ) =/= (/) )
74 73 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X = y ) -> -. ( A i^i C ) = (/) )
75 48 74 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. X = y )
76 75 neqned 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> X =/= y )
77 76 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> X =/= y )
78 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> y e. ( X I r ) )
79 1 9 2 22 29 43 25 77 78 btwnlng3 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> r e. ( X L y ) )
80 39 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> B e. ran L )
81 14 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> X e. B )
82 40 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> y e. B )
83 1 9 2 21 28 42 76 76 80 81 82 tglinethru 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> B = ( X L y ) )
84 83 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> B = ( X L y ) )
85 79 84 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> r e. B )
86 81 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> X e. B )
87 2 30 3 22 32 38 85 86 prlnghpg 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> r ( ( hpG ` G ) ` A ) X )
88 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> s e. P )
89 13 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> A .|| C )
90 89 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> A .|| C )
91 46 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> A =/= C )
92 91 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> A =/= C )
93 15 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> X e. C )
94 93 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> X e. C )
95 simpllr 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> v e. P )
96 95 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> v e. P )
97 96 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> v e. P )
98 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> X =/= v )
99 98 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> X =/= v )
100 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> v e. ( X I s ) )
101 1 9 2 22 29 97 88 99 100 btwnlng3 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> s e. ( X L v ) )
102 11 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> C e. ran L )
103 20 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> G e. TarskiG )
104 53 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> W e. P )
105 27 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> X e. P )
106 95 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> v e. P )
107 62 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> W =/= X )
108 simplr 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> X e. ( W I v ) )
109 108 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> X e. ( W I v ) )
110 1 9 2 103 104 105 106 107 109 btwnlng3 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> v e. ( W L X ) )
111 69 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> C = ( W L X ) )
112 110 111 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) -> v e. C )
113 112 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> v e. C )
114 1 9 2 21 28 96 98 98 102 93 113 tglinethru 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> C = ( X L v ) )
115 114 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> C = ( X L v ) )
116 101 115 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> s e. C )
117 2 30 3 22 90 92 94 116 prlnghpg 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> X ( ( hpG ` G ) ` A ) s )
118 1 9 2 22 24 25 8 29 87 88 117 hpgtr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> r ( ( hpG ` G ) ` A ) s )
119 118 3anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) ) -> r ( ( hpG ` G ) ` A ) s )
120 eqid 
 |-  ( dist ` G ) = ( dist ` G )
121 16 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> T e. A )
122 121 ad5antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> T e. A )
123 1 9 2 8 22 24 25 29 87 hpgne1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> -. r e. A )
124 2 30 3 22 90 92 116 94 prlnghpg 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> s ( ( hpG ` G ) ` A ) X )
125 1 9 2 8 22 24 88 29 124 hpgne1 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> -. s e. A )
126 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> T e. ( r I s ) )
127 1 120 9 8 25 88 122 123 125 126 islnoppd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> r Q s )
128 1 9 2 8 22 24 25 88 127 lnoppnhpg 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ y e. ( X I r ) ) /\ v e. ( X I s ) ) /\ T e. ( r I s ) ) -> -. r ( ( hpG ` G ) ` A ) s )
129 128 3anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) /\ ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) ) -> -. r ( ( hpG ` G ) ` A ) s )
130 119 129 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ r e. P ) /\ s e. P ) -> -. ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) )
131 130 anasss 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ ( r e. P /\ s e. P ) ) -> -. ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) )
132 131 ralrimivva 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> A. r e. P A. s e. P -. ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) )
133 ralnex2 
 |-  ( A. r e. P A. s e. P -. ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) <-> -. E. r e. P E. s e. P ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) )
134 132 133 sylib 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. E. r e. P E. s e. P ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) )
135 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> G e. TarskiGE )
136 28 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> X e. P )
137 21 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> G e. TarskiG )
138 80 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> B e. ran L )
139 82 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> y e. B )
140 1 2 9 137 138 139 tglnpt 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> y e. P )
141 96 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> v e. P )
142 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> z e. P )
143 142 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> z e. P )
144 57 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> T e. P )
145 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> z e. ( X I T ) )
146 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> z e. ( y I v ) )
147 47 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> ( A i^i C ) = (/) )
148 16 ad9antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> T e. A )
149 21 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> G e. TarskiG )
150 104 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> W e. P )
151 42 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> y e. P )
152 57 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> T e. P )
153 59 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. W e. B )
154 nelne2 
 |-  ( ( y e. B /\ -. W e. B ) -> y =/= W )
155 82 153 154 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> y =/= W )
156 155 necomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> W =/= y )
157 156 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> W =/= y )
158 65 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> y e. ( W I T ) )
159 1 9 2 149 150 151 152 157 158 btwnlng3 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> T e. ( W L y ) )
160 104 adantr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> W e. P )
161 81 153 elnelneq2d 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. X = W )
162 21 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> G e. TarskiG )
163 160 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> W e. P )
164 28 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> X e. P )
165 109 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> X e. ( W I v ) )
166 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> W = v )
167 166 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> ( W I W ) = ( W I v ) )
168 165 167 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> X e. ( W I W ) )
169 1 120 9 162 163 164 168 axtgbtwnid 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> W = X )
170 169 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ W = v ) -> X = W )
171 161 170 mtand 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. W = v )
172 171 neqned 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> W =/= v )
173 51 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> W e. C )
174 1 9 2 21 160 96 172 172 102 173 113 tglinethru 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> C = ( W L v ) )
175 174 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> C = ( W L v ) )
176 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> y = v )
177 176 oveq2d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> ( W L y ) = ( W L v ) )
178 175 177 eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> C = ( W L y ) )
179 159 178 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> T e. C )
180 148 179 elind 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> T e. ( A i^i C ) )
181 180 ne0d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> ( A i^i C ) =/= (/) )
182 181 neneqd 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ y = v ) -> -. ( A i^i C ) = (/) )
183 147 182 pm2.65da 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. y = v )
184 183 neqned 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> y =/= v )
185 simplr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> z e. ( y I v ) )
186 1 9 2 21 42 96 142 184 185 btwnlng1 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> z e. ( y L v ) )
187 18 neneqd 
 |-  ( ph -> -. B = C )
188 187 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. B = C )
189 21 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> G e. TarskiG )
190 28 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> X e. P )
191 96 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> v e. P )
192 98 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> X =/= v )
193 42 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> y e. P )
194 76 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> X =/= y )
195 1 9 2 189 190 193 194 tgelrnln 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> ( X L y ) e. ran L )
196 1 9 2 189 190 193 194 tglinerflx1 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> X e. ( X L y ) )
197 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> X e. ( y L v ) )
198 184 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> y =/= v )
199 1 9 2 189 190 193 191 194 197 198 lnrot2 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> v e. ( X L y ) )
200 1 9 2 189 190 191 192 192 195 196 199 tglinethru 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> ( X L y ) = ( X L v ) )
201 83 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> B = ( X L y ) )
202 114 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> C = ( X L v ) )
203 200 201 202 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ X e. ( y L v ) ) -> B = C )
204 188 203 mtand 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. X e. ( y L v ) )
205 nelne2 
 |-  ( ( z e. ( y L v ) /\ -. X e. ( y L v ) ) -> z =/= X )
206 186 204 205 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> z =/= X )
207 206 necomd 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> X =/= z )
208 207 adantr 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> X =/= z )
209 1 120 9 135 136 140 141 143 144 145 146 208 axtgeucl 
 |-  ( ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) /\ G e. TarskiGE ) -> E. r e. P E. s e. P ( y e. ( X I r ) /\ v e. ( X I s ) /\ T e. ( r I s ) ) )
210 134 209 mtand 
 |-  ( ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ z e. ( y I v ) ) /\ z e. ( X I T ) ) -> -. G e. TarskiGE )
211 210 anasss 
 |-  ( ( ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) /\ z e. P ) /\ ( z e. ( y I v ) /\ z e. ( X I T ) ) ) -> -. G e. TarskiGE )
212 1 120 9 20 53 41 57 65 tgbtwncom 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> y e. ( T I W ) )
213 1 120 9 20 53 27 95 108 tgbtwncom 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> X e. ( v I W ) )
214 1 120 9 20 57 95 53 41 27 212 213 axtgpasch 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> E. z e. P ( z e. ( y I v ) /\ z e. ( X I T ) ) )
215 211 214 r19.29a 
 |-  ( ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ X e. ( W I v ) ) /\ X =/= v ) -> -. G e. TarskiGE )
216 215 anasss 
 |-  ( ( ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) /\ v e. P ) /\ ( X e. ( W I v ) /\ X =/= v ) ) -> -. G e. TarskiGE )
217 1 fvexi 
 |-  P e. _V
218 217 a1i 
 |-  ( ph -> P e. _V )
219 218 26 52 61 nehash2 
 |-  ( ph -> 2 <_ ( # ` P ) )
220 1 120 9 4 52 26 219 tgbtwndiff 
 |-  ( ph -> E. v e. P ( X e. ( W I v ) /\ X =/= v ) )
221 220 ad2antrr 
 |-  ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) -> E. v e. P ( X e. ( W I v ) /\ X =/= v ) )
222 216 221 r19.29a 
 |-  ( ( ( ph /\ y e. B ) /\ y e. ( W I T ) ) -> -. G e. TarskiGE )
223 1 120 9 7 52 56 islnopp 
 |-  ( ph -> ( W O T <-> ( ( -. W e. B /\ -. T e. B ) /\ E. y e. B y e. ( W I T ) ) ) )
224 19 223 mpbid 
 |-  ( ph -> ( ( -. W e. B /\ -. T e. B ) /\ E. y e. B y e. ( W I T ) ) )
225 224 simprd 
 |-  ( ph -> E. y e. B y e. ( W I T ) )
226 222 225 r19.29a 
 |-  ( ph -> -. G e. TarskiGE )