Metamath Proof Explorer

Theorem ipotset

Description: Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015)

Ref Expression
Hypotheses ipoval.i 
|- I = ( toInc ` F )
ipole.l 
|- .<_ = ( le ` I )
Assertion ipotset 
|- ( F e. V -> ( ordTop ` .<_ ) = ( TopSet ` I ) )

Proof

Step Hyp Ref Expression
1 ipoval.i 
 |-  I = ( toInc ` F )
2 ipole.l 
 |-  .<_ = ( le ` I )
3 fvex 
 |-  ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) e. _V
4 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 >.
5 tsetid 
 |-  TopSet = Slot ( TopSet ` ndx )
6 snsspr2 
 |-  { <. ( 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 ) } ) >. }
7 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 ) = (/) } ) >. } )
8 6 7 sstri 
 |-  { <. ( 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 ) = (/) } ) >. } )
9 4 5 8 strfv 
 |-  ( ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) e. _V -> ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) = ( TopSet ` ( { <. ( 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 3 9 ax-mp 
 |-  ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) = ( TopSet ` ( { <. ( 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 1 ipolerval 
 |-  ( F e. V -> { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = ( le ` I ) )
12 2 11 eqtr4id 
 |-  ( F e. V -> .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } )
13 12 fveq2d 
 |-  ( F e. V -> ( ordTop ` .<_ ) = ( ordTop ` { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } ) )
14 eqid 
 |-  { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
15 1 14 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 ) = (/) } ) >. } ) )
16 15 fveq2d 
 |-  ( F e. V -> ( TopSet ` I ) = ( TopSet ` ( { <. ( 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 10 13 16 3eqtr4a 
 |-  ( F e. V -> ( ordTop ` .<_ ) = ( TopSet ` I ) )