Metamath Proof Explorer

Theorem filnetlem2

Description: Lemma for filnet . The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009) (Revised by Mario Carneiro, 8-Aug-2015)

Ref Expression
Hypotheses filnet.h 
|- H = U_ n e. F ( { n } X. n )
filnet.d 
|- D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }
Assertion filnetlem2 
|- ( ( _I |` H ) C_ D /\ D C_ ( H X. H ) )

Proof

Step Hyp Ref Expression
1 filnet.h 
 |-  H = U_ n e. F ( { n } X. n )
2 filnet.d 
 |-  D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }
3 idref 
 |-  ( ( _I |` H ) C_ D <-> A. z e. H z D z )
4 ssid 
 |-  ( 1st ` z ) C_ ( 1st ` z )
5 vex 
 |-  z e. _V
6 1 2 5 5 filnetlem1 
 |-  ( z D z <-> ( ( z e. H /\ z e. H ) /\ ( 1st ` z ) C_ ( 1st ` z ) ) )
7 4 6 mpbiran2 
 |-  ( z D z <-> ( z e. H /\ z e. H ) )
8 7 biimpri 
 |-  ( ( z e. H /\ z e. H ) -> z D z )
9 8 anidms 
 |-  ( z e. H -> z D z )
10 3 9 mprgbir 
 |-  ( _I |` H ) C_ D
11 opabssxp 
 |-  { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) } C_ ( H X. H )
12 2 11 eqsstri 
 |-  D C_ ( H X. H )
13 10 12 pm3.2i 
 |-  ( ( _I |` H ) C_ D /\ D C_ ( H X. H ) )