Metamath Proof Explorer

Theorem ipole

Description: Weak order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses ipoval.i 
|- I = ( toInc ` F )
ipole.l 
|- .<_ = ( le ` I )
Assertion ipole 
|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .<_ Y <-> X C_ Y ) )

Proof

Step Hyp Ref Expression
1 ipoval.i 
 |-  I = ( toInc ` F )
2 ipole.l 
 |-  .<_ = ( le ` I )
3 preq12 
 |-  ( ( x = X /\ y = Y ) -> { x , y } = { X , Y } )
4 3 sseq1d 
 |-  ( ( x = X /\ y = Y ) -> ( { x , y } C_ F <-> { X , Y } C_ F ) )
5 sseq12 
 |-  ( ( x = X /\ y = Y ) -> ( x C_ y <-> X C_ Y ) )
6 4 5 anbi12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( { x , y } C_ F /\ x C_ y ) <-> ( { X , Y } C_ F /\ X C_ Y ) ) )
7 eqid 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
8 6 7 brabga 
 |-  ( ( X e. F /\ Y e. F ) -> ( X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y <-> ( { X , Y } C_ F /\ X C_ Y ) ) )
9 8 3adant1 
 |-  ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y <-> ( { X , Y } C_ F /\ X C_ Y ) ) )
10 1 ipolerval 
 |-  ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` I ) )
11 2 10 eqtr4id 
 |-  ( F e. V -> .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } )
12 11 breqd 
 |-  ( F e. V -> ( X .<_ Y <-> X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y ) )
13 12 3ad2ant1 
 |-  ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .<_ Y <-> X { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } Y ) )
14 prssi 
 |-  ( ( X e. F /\ Y e. F ) -> { X , Y } C_ F )
15 14 3adant1 
 |-  ( ( F e. V /\ X e. F /\ Y e. F ) -> { X , Y } C_ F )
16 15 biantrurd 
 |-  ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X C_ Y <-> ( { X , Y } C_ F /\ X C_ Y ) ) )
17 9 13 16 3bitr4d 
 |-  ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .<_ Y <-> X C_ Y ) )