Metamath Proof Explorer

Theorem filnetlem1

Description: Lemma for filnet . Change variables. (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 ) ) }
filnetlem1.a 
|- A e. _V
filnetlem1.b 
|- B e. _V
Assertion filnetlem1 
|- ( A D B <-> ( ( A e. H /\ B e. H ) /\ ( 1st ` B ) C_ ( 1st ` A ) ) )

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 filnetlem1.a 
 |-  A e. _V
4 filnetlem1.b 
 |-  B e. _V
5 fveq2 
 |-  ( x = A -> ( 1st ` x ) = ( 1st ` A ) )
6 5 sseq2d 
 |-  ( x = A -> ( ( 1st ` y ) C_ ( 1st ` x ) <-> ( 1st ` y ) C_ ( 1st ` A ) ) )
7 fveq2 
 |-  ( y = B -> ( 1st ` y ) = ( 1st ` B ) )
8 7 sseq1d 
 |-  ( y = B -> ( ( 1st ` y ) C_ ( 1st ` A ) <-> ( 1st ` B ) C_ ( 1st ` A ) ) )
9 6 8 sylan9bb 
 |-  ( ( x = A /\ y = B ) -> ( ( 1st ` y ) C_ ( 1st ` x ) <-> ( 1st ` B ) C_ ( 1st ` A ) ) )
10 9 2 brab2a 
 |-  ( A D B <-> ( ( A e. H /\ B e. H ) /\ ( 1st ` B ) C_ ( 1st ` A ) ) )