Metamath Proof Explorer

Theorem ipolerval

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

Ref Expression
Hypothesis ipoval.i 
|- I = ( toInc ` F )
Assertion ipolerval 
|- ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` I ) )

Proof

Step Hyp Ref Expression
1 ipoval.i 
 |-  I = ( toInc ` F )
2 vex 
 |-  x e. _V
3 vex 
 |-  y e. _V
4 2 3 prss 
 |-  ( ( x e. F /\ y e. F ) <-> { x , y } C_ F )
5 4 biranri 
 |-  ( ( { x , y } C_ F /\ x C_ y ) -> ( x e. F /\ y e. F ) )
6 5 ssopab2i 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } C_ { <. x , y >. | ( x e. F /\ y e. F ) }
7 df-xp 
 |-  ( F X. F ) = { <. x , y >. | ( x e. F /\ y e. F ) }
8 6 7 sseqtrri 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } C_ ( F X. F )
9 sqxpexg 
 |-  ( F e. V -> ( F X. F ) e. _V )
10 ssexg 
 |-  ( ( { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } C_ ( F X. F ) /\ ( F X. F ) e. _V ) -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } e. _V )
11 8 9 10 sylancr 
 |-  ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } e. _V )
12 ipostr 
 |-  ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. } u. { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) Struct <. 1 , ; 1 1 >.
13 pleid 
 |-  le = Slot ( le ` ndx )
14 snsspr1 
 |-  { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. } C_ { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. }
15 ssun2 
 |-  { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } C_ ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. } u. { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } )
16 14 15 sstri 
 |-  { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. } C_ ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. } u. { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } )
17 12 13 16 strfv 
 |-  ( { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } e. _V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. } u. { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) ) )
18 11 17 syl 
 |-  ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. } u. { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) ) )
19 eqid 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
20 1 19 ipoval 
 |-  ( F e. V -> I = ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. } u. { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )
21 20 fveq2d 
 |-  ( F e. V -> ( le ` I ) = ( le ` ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. } u. { <. ( le ` ndx ) , { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) ) )
22 18 21 eqtr4d 
 |-  ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` I ) )