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 ) )