Metamath Proof Explorer

Theorem outsideofeu

Description: Given a nondegenerate ray, there is a unique point congruent to the segment B C lying on the ray A R . Theorem 6.11 of Schwabhauser p. 44. (Contributed by Scott Fenton, 23-Oct-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion outsideofeu 
|- ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( R =/= A /\ B =/= C ) -> E! x e. ( EE ` N ) ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) ) )

Proof

Step Hyp Ref Expression
1 segcon2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> E. x e. ( EE ` N ) ( ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) /\ <. A , x >. Cgr <. B , C >. ) )
2 1 adantr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) -> E. x e. ( EE ` N ) ( ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) /\ <. A , x >. Cgr <. B , C >. ) )
3 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> N e. NN )
4 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> A e. ( EE ` N ) )
5 simpr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> x e. ( EE ` N ) )
6 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> R e. ( EE ` N ) )
7 broutsideof2 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) /\ R e. ( EE ` N ) ) ) -> ( A OutsideOf <. x , R >. <-> ( x =/= A /\ R =/= A /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) )
8 3 4 5 6 7 syl13anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( A OutsideOf <. x , R >. <-> ( x =/= A /\ R =/= A /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) )
9 8 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) ) -> ( A OutsideOf <. x , R >. <-> ( x =/= A /\ R =/= A /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) )
10 simp3 
 |-  ( ( x =/= A /\ R =/= A /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) -> ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) )
11 simpllr 
 |-  ( ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) -> B =/= C )
12 11 adantl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> B =/= C )
13 simprlr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> <. A , x >. Cgr <. B , C >. )
14 simp2l 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
15 14 anim1i 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( A e. ( EE ` N ) /\ x e. ( EE ` N ) ) )
16 simpl3 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) )
17 cgrdegen 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ x e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( <. A , x >. Cgr <. B , C >. -> ( A = x <-> B = C ) ) )
18 3 15 16 17 syl3anc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) -> ( <. A , x >. Cgr <. B , C >. -> ( A = x <-> B = C ) ) )
19 18 adantr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> ( <. A , x >. Cgr <. B , C >. -> ( A = x <-> B = C ) ) )
20 13 19 mpd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> ( A = x <-> B = C ) )
21 20 necon3bid 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> ( A =/= x <-> B =/= C ) )
22 12 21 mpbird 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> A =/= x )
23 22 necomd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> x =/= A )
24 simplll 
 |-  ( ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) -> R =/= A )
25 24 adantl 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> R =/= A )
26 simprr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) )
27 23 25 26 3jca 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) -> ( x =/= A /\ R =/= A /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) )
28 27 expr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) ) -> ( ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) -> ( x =/= A /\ R =/= A /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) ) )
29 10 28 impbid2 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) ) -> ( ( x =/= A /\ R =/= A /\ ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) <-> ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) )
30 9 29 bitrd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) ) -> ( A OutsideOf <. x , R >. <-> ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) ) )
31 orcom 
 |-  ( ( x Btwn <. A , R >. \/ R Btwn <. A , x >. ) <-> ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) )
32 30 31 bitrdi 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( ( R =/= A /\ B =/= C ) /\ <. A , x >. Cgr <. B , C >. ) ) -> ( A OutsideOf <. x , R >. <-> ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) ) )
33 32 expr 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( R =/= A /\ B =/= C ) ) -> ( <. A , x >. Cgr <. B , C >. -> ( A OutsideOf <. x , R >. <-> ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) ) ) )
34 33 pm5.32rd 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ x e. ( EE ` N ) ) /\ ( R =/= A /\ B =/= C ) ) -> ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) <-> ( ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) /\ <. A , x >. Cgr <. B , C >. ) ) )
35 34 an32s 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) /\ x e. ( EE ` N ) ) -> ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) <-> ( ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) /\ <. A , x >. Cgr <. B , C >. ) ) )
36 35 rexbidva 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) -> ( E. x e. ( EE ` N ) ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) <-> E. x e. ( EE ` N ) ( ( R Btwn <. A , x >. \/ x Btwn <. A , R >. ) /\ <. A , x >. Cgr <. B , C >. ) ) )
37 2 36 mpbird 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) -> E. x e. ( EE ` N ) ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) )
38 simpl1 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> N e. NN )
39 simpl2l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> A e. ( EE ` N ) )
40 simpl2r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> R e. ( EE ` N ) )
41 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> B e. ( EE ` N ) )
42 39 40 41 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( A e. ( EE ` N ) /\ R e. ( EE ` N ) /\ B e. ( EE ` N ) ) )
43 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> C e. ( EE ` N ) )
44 simprl 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> x e. ( EE ` N ) )
45 simprr 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> y e. ( EE ` N ) )
46 43 44 45 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( C e. ( EE ` N ) /\ x e. ( EE ` N ) /\ y e. ( EE ` N ) ) )
47 38 42 46 3jca 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) )
48 simpr 
 |-  ( ( ( R =/= A /\ B =/= C ) /\ ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) ) -> ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) )
49 outsideofeq 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) -> ( ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) -> x = y ) )
50 49 imp 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( C e. ( EE ` N ) /\ x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) /\ ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) ) -> x = y )
51 47 48 50 syl2an 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) ) /\ ( ( R =/= A /\ B =/= C ) /\ ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) ) ) -> x = y )
52 51 an4s 
 |-  ( ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) /\ ( ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) /\ ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) ) ) -> x = y )
53 52 exp32 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) -> ( ( x e. ( EE ` N ) /\ y e. ( EE ` N ) ) -> ( ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) -> x = y ) ) )
54 53 ralrimivv 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) -> A. x e. ( EE ` N ) A. y e. ( EE ` N ) ( ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) -> x = y ) )
55 opeq1 
 |-  ( x = y -> <. x , R >. = <. y , R >. )
56 55 breq2d 
 |-  ( x = y -> ( A OutsideOf <. x , R >. <-> A OutsideOf <. y , R >. ) )
57 opeq2 
 |-  ( x = y -> <. A , x >. = <. A , y >. )
58 57 breq1d 
 |-  ( x = y -> ( <. A , x >. Cgr <. B , C >. <-> <. A , y >. Cgr <. B , C >. ) )
59 56 58 anbi12d 
 |-  ( x = y -> ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) <-> ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) )
60 59 reu4 
 |-  ( E! x e. ( EE ` N ) ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) <-> ( E. x e. ( EE ` N ) ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ A. x e. ( EE ` N ) A. y e. ( EE ` N ) ( ( ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) /\ ( A OutsideOf <. y , R >. /\ <. A , y >. Cgr <. B , C >. ) ) -> x = y ) ) )
61 37 54 60 sylanbrc 
 |-  ( ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) /\ ( R =/= A /\ B =/= C ) ) -> E! x e. ( EE ` N ) ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) )
62 61 ex 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ R e. ( EE ` N ) ) /\ ( B e. ( EE ` N ) /\ C e. ( EE ` N ) ) ) -> ( ( R =/= A /\ B =/= C ) -> E! x e. ( EE ` N ) ( A OutsideOf <. x , R >. /\ <. A , x >. Cgr <. B , C >. ) ) )