Metamath Proof Explorer

Theorem seglerflx

Description: Segment comparison is reflexive. Theorem 5.7 of Schwabhauser p. 42. (Contributed by Scott Fenton, 11-Oct-2013)

Ref Expression
Assertion seglerflx 
|- ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Seg<_ <. A , B >. )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B e. ( EE ` N ) )
2 btwntriv2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> B Btwn <. A , B >. )
3 cgrrflx 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Cgr <. A , B >. )
4 breq1 
 |-  ( y = B -> ( y Btwn <. A , B >. <-> B Btwn <. A , B >. ) )
5 opeq2 
 |-  ( y = B -> <. A , y >. = <. A , B >. )
6 5 breq2d 
 |-  ( y = B -> ( <. A , B >. Cgr <. A , y >. <-> <. A , B >. Cgr <. A , B >. ) )
7 4 6 anbi12d 
 |-  ( y = B -> ( ( y Btwn <. A , B >. /\ <. A , B >. Cgr <. A , y >. ) <-> ( B Btwn <. A , B >. /\ <. A , B >. Cgr <. A , B >. ) ) )
8 7 rspcev 
 |-  ( ( B e. ( EE ` N ) /\ ( B Btwn <. A , B >. /\ <. A , B >. Cgr <. A , B >. ) ) -> E. y e. ( EE ` N ) ( y Btwn <. A , B >. /\ <. A , B >. Cgr <. A , y >. ) )
9 1 2 3 8 syl12anc 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> E. y e. ( EE ` N ) ( y Btwn <. A , B >. /\ <. A , B >. Cgr <. A , y >. ) )
10 simp1 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> N e. NN )
11 simp2 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> A e. ( EE ` N ) )
12 brsegle 
 |-  ( ( N e. NN /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) /\ ( A e. ( EE ` N ) /\ B e. ( EE ` N ) ) ) -> ( <. A , B >. Seg<_ <. A , B >. <-> E. y e. ( EE ` N ) ( y Btwn <. A , B >. /\ <. A , B >. Cgr <. A , y >. ) ) )
13 10 11 1 11 1 12 syl122anc 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> ( <. A , B >. Seg<_ <. A , B >. <-> E. y e. ( EE ` N ) ( y Btwn <. A , B >. /\ <. A , B >. Cgr <. A , y >. ) ) )
14 9 13 mpbird 
 |-  ( ( N e. NN /\ A e. ( EE ` N ) /\ B e. ( EE ` N ) ) -> <. A , B >. Seg<_ <. A , B >. )