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 simpl 
 |-  ( ( { x , y } C_ f /\ x C_ y ) -> { x , y } C_ f )
7 vex 
 |-  x e. _V
8 vex 
 |-  y e. _V
9 7 8 prss 
 |-  ( ( x e. f /\ y e. f ) <-> { x , y } C_ f )
10 6 9 sylibr 
 |-  ( ( { x , y } C_ f /\ x C_ y ) -> ( x e. f /\ y e. f ) )
11 10 ssopab2i 
 |-  { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } C_ { <. x , y >. | ( x e. f /\ y e. f ) }
12 df-xp 
 |-  ( f X. f ) = { <. x , y >. | ( x e. f /\ y e. f ) }
13 11 12 sseqtrri 
 |-  { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } C_ ( f X. f )
14 5 13 ssexi 
 |-  { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } e. _V
15 14 a1i 
 |-  ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } e. _V )
16 sseq2 
 |-  ( f = F -> ( { x , y } C_ f <-> { x , y } C_ F ) )
17 16 anbi1d 
 |-  ( f = F -> ( ( { x , y } C_ f /\ x C_ y ) <-> ( { x , y } C_ F /\ x C_ y ) ) )
18 17 opabbidv 
 |-  ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } )
19 18 2 eqtr4di 
 |-  ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } = .<_ )
20 simpl 
 |-  ( ( f = F /\ o = .<_ ) -> f = F )
21 20 opeq2d 
 |-  ( ( f = F /\ o = .<_ ) -> <. ( Base ` ndx ) , f >. = <. ( Base ` ndx ) , F >. )
22 simpr 
 |-  ( ( f = F /\ o = .<_ ) -> o = .<_ )
23 22 fveq2d 
 |-  ( ( f = F /\ o = .<_ ) -> ( ordTop ` o ) = ( ordTop ` .<_ ) )
24 23 opeq2d 
 |-  ( ( f = F /\ o = .<_ ) -> <. ( TopSet ` ndx ) , ( ordTop ` o ) >. = <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. )
25 21 24 preq12d 
 |-  ( ( f = F /\ o = .<_ ) -> { <. ( Base ` ndx ) , f >. , <. ( TopSet ` ndx ) , ( ordTop ` o ) >. } = { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } )
26 22 opeq2d 
 |-  ( ( f = F /\ o = .<_ ) -> <. ( le ` ndx ) , o >. = <. ( le ` ndx ) , .<_ >. )
27 id 
 |-  ( f = F -> f = F )
28 rabeq 
 |-  ( f = F -> { y e. f | ( y i^i x ) = (/) } = { y e. F | ( y i^i x ) = (/) } )
29 28 unieqd 
 |-  ( f = F -> U. { y e. f | ( y i^i x ) = (/) } = U. { y e. F | ( y i^i x ) = (/) } )
30 27 29 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 ) = (/) } ) )
31 30 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 ) = (/) } ) )
32 31 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 ) = (/) } ) >. )
33 26 32 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 ) = (/) } ) >. } )
34 25 33 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 ) = (/) } ) >. } ) )
35 15 19 34 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 ) = (/) } ) >. } ) )
36 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 ) = (/) } ) >. } ) )
37 prex 
 |-  { <. ( Base ` ndx ) , F >. , <. ( TopSet ` ndx ) , ( ordTop ` .<_ ) >. } e. _V
38 prex 
 |-  { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } e. _V
39 37 38 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
40 35 36 39 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 ) = (/) } ) >. } ) )
41 1 40 syl5eq 
 |-  ( 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 ) = (/) } ) >. } ) )
42 3 41 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 ) = (/) } ) >. } ) )