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 simpl 
 |-  ( ( { x , y } C_ F /\ x C_ y ) -> { x , y } C_ F )
3 vex 
 |-  x e. _V
4 vex 
 |-  y e. _V
5 3 4 prss 
 |-  ( ( x e. F /\ y e. F ) <-> { x , y } C_ F )
6 2 5 sylibr 
 |-  ( ( { x , y } C_ F /\ x C_ y ) -> ( x e. F /\ y e. F ) )
7 6 ssopab2i 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } C_ { <. x , y >. | ( x e. F /\ y e. F ) }
8 df-xp 
 |-  ( F X. F ) = { <. x , y >. | ( x e. F /\ y e. F ) }
9 7 8 sseqtrri 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } C_ ( F X. F )
10 sqxpexg 
 |-  ( F e. V -> ( F X. F ) e. _V )
11 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 )
12 9 10 11 sylancr 
 |-  ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } e. _V )
13 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 >.
14 pleid 
 |-  le = Slot ( le ` ndx )
15 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 ) = (/) } ) >. }
16 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 ) = (/) } ) >. } )
17 15 16 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 ) = (/) } ) >. } )
18 13 14 17 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 ) = (/) } ) >. } ) ) )
19 12 18 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 ) = (/) } ) >. } ) ) )
20 eqid 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
21 1 20 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 ) = (/) } ) >. } ) )
22 21 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 ) = (/) } ) >. } ) ) )
23 19 22 eqtr4d 
 |-  ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` I ) )