Metamath Proof Explorer

Theorem ipoval

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

Ref Expression
Hypotheses ipoval.i 
|- I = ( toInc ` F )
ipoval.l 
|- .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
Assertion ipoval 
|- ( F e. V -> I = ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )

Proof

Step Hyp Ref Expression
1 ipoval.i 
 |-  I = ( toInc ` F )
2 ipoval.l 
 |-  .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
3 elex 
 |-  ( F e. V -> F e. _V )
4 vex 
 |-  f e. _V
5 4 4 xpex 
 |-  ( f X. f ) e. _V
6 vex 
 |-  x e. _V
7 vex 
 |-  y e. _V
8 6 7 prss 
 |-  ( ( x e. f /\ y e. f ) <-> { x , y } C_ f )
9 8 biranri 
 |-  ( ( { x , y } C_ f /\ x C_ y ) -> ( x e. f /\ y e. f ) )
10 9 ssopab2i 
 |-  { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } C_ { <. x , y >. | ( x e. f /\ y e. f ) }
11 df-xp 
 |-  ( f X. f ) = { <. x , y >. | ( x e. f /\ y e. f ) }
12 10 11 sseqtrri 
 |-  { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } C_ ( f X. f )
13 5 12 ssexi 
 |-  { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } e. _V
14 13 a1i 
 |-  ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } e. _V )
15 sseq2 
 |-  ( f = F -> ( { x , y } C_ f <-> { x , y } C_ F ) )
16 15 anbi1d 
 |-  ( f = F -> ( ( { x , y } C_ f /\ x C_ y ) <-> ( { x , y } C_ F /\ x C_ y ) ) )
17 16 opabbidv 
 |-  ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } )
18 17 2 eqtr4di 
 |-  ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } = .<_ )
19 simpl 
 |-  ( ( f = F /\ o = .<_ ) -> f = F )
20 19 opeq2d 
 |-  ( ( f = F /\ o = .<_ ) -> <. ( Base ` ndx ) , f >. = <. ( Base ` ndx ) , F >. )
21 simpr 
 |-  ( ( f = F /\ o = .<_ ) -> o = .<_ )
22 21 fveq2d 
 |-  ( ( f = F /\ o = .<_ ) -> ( ordTop ` o ) = ( ordTop ` .<_ ) )
23 22 opeq2d 
 |-  ( ( f = F /\ o = .<_ ) -> <. ( TopSet ` ndx ) , ( ordTop ` o ) >. = <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. )
24 20 23 preq12d 
 |-  ( ( f = F /\ o = .<_ ) -> { <. ( Base ` ndx ) , f >. , <. ( TopSet ` ndx ) , ( ordTop ` o ) >. } = { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } )
25 21 opeq2d 
 |-  ( ( f = F /\ o = .<_ ) -> <. ( le ` ndx ) , o >. = <. ( le ` ndx ) , .<_ >. )
26 id 
 |-  ( f = F -> f = F )
27 rabeq 
 |-  ( f = F -> { y e. f | ( y i^i x ) = (/) } = { y e. F | ( y i^i x ) = (/) } )
28 27 unieqd 
 |-  ( f = F -> U. { y e. f | ( y i^i x ) = (/) } = U. { y e. F | ( y i^i x ) = (/) } )
29 26 28 mpteq12dv 
 |-  ( f = F -> ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) = ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) )
30 29 adantr 
 |-  ( ( f = F /\ o = .<_ ) -> ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) = ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) )
31 30 opeq2d 
 |-  ( ( f = F /\ o = .<_ ) -> <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. = <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. )
32 25 31 preq12d 
 |-  ( ( f = F /\ o = .<_ ) -> { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. } = { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } )
33 24 32 uneq12d 
 |-  ( ( f = F /\ o = .<_ ) -> ( { <. ( Base ` ndx ) , f >. , <. ( TopSet ` ndx ) , ( ordTop ` o ) >. } u. { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. } ) = ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )
34 14 18 33 csbied2 
 |-  ( f = F -> [_ { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } / o ]_ ( { <. ( Base ` ndx ) , f >. , <. ( TopSet ` ndx ) , ( ordTop ` o ) >. } u. { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. } ) = ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )
35 df-ipo 
 |-  toInc = ( f e. _V |-> [_ { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } / o ]_ ( { <. ( Base ` ndx ) , f >. , <. ( TopSet ` ndx ) , ( ordTop ` o ) >. } u. { <. ( le ` ndx ) , o >. , <. ( oc ` ndx ) , ( x e. f |-> U. { y e. f | ( y i^i x ) = (/) } ) >. } ) )
36 prex 
 |-  { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } e. _V
37 prex 
 |-  { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } e. _V
38 36 37 unex 
 |-  ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) e. _V
39 34 35 38 fvmpt 
 |-  ( F e. _V -> ( toInc ` F ) = ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )
40 1 39 eqtrid 
 |-  ( F e. _V -> I = ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )
41 3 40 syl 
 |-  ( F e. V -> I = ( { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } u. { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } ) )