Metamath Proof Explorer

Theorem ipobas

Description: Base set of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015) (Revised by Mario Carneiro, 25-Oct-2015)

Ref Expression
Hypothesis ipoval.i 
|- I = ( toInc ` F )
Assertion ipobas 
|- ( F e. V -> F = ( Base ` I ) )

Proof

Step Hyp Ref Expression
1 ipoval.i 
 |-  I = ( toInc ` F )
2 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 >.
3 baseid 
 |-  Base = Slot ( Base ` ndx )
4 snsspr1 
 |-  { <. ( Base ` ndx ) , F >. } C_ { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) >. }
5 ssun1 
 |-  { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` { <. 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 ) = (/) } ) >. } )
6 4 5 sstri 
 |-  { <. ( Base ` ndx ) , F >. } 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 ) = (/) } ) >. } )
7 2 3 6 strfv 
 |-  ( F e. V -> F = ( Base ` ( { <. ( 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 ) = (/) } ) >. } ) ) )
8 eqid 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
9 1 8 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 ) = (/) } ) >. } ) )
10 9 fveq2d 
 |-  ( F e. V -> ( Base ` I ) = ( Base ` ( { <. ( 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 ) = (/) } ) >. } ) ) )
11 7 10 eqtr4d 
 |-  ( F e. V -> F = ( Base ` I ) )