Theorem ipoval 17154

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

Hypotheses

Ref	Expression
ipoval.i	|- I = (toInc ` F )
ipoval.l	|- .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }

Assertion

Ref	Expression
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 ) = (/) } ) >. } ) )

Distinct variable groups:   x, y, F   x, I, y   x, V, y

Allowed substitution hints:   .<_ ( x, y)

Proof of Theorem ipoval

Dummy variables f o are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elex 3212	. 2 |- ( F e. V -> F e. _V )
2		ipoval.i	. . 3 |- I = (toInc ` F )
3		vex 3203	. . . . . . . 8 |- f e. _V
4	3, 3	xpex 6962	. . . . . . 7 |- ( f X. f ) e. _V
5		simpl 473	. . . . . . . . . 10 |- ( ( { x , y } C_ f /\ x C_ y ) -> { x , y } C_ f )
6		vex 3203	. . . . . . . . . . 11 |- x e. _V
7		vex 3203	. . . . . . . . . . 11 |- y e. _V
8	6, 7	prss 4351	. . . . . . . . . 10 |- ( ( x e. f /\ y e. f ) <-> { x , y } C_ f )
9	5, 8	sylibr 224	. . . . . . . . 9 |- ( ( { x , y } C_ f /\ x C_ y ) -> ( x e. f /\ y e. f ) )
10	9	ssopab2i 5003	. . . . . . . 8 |- { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } C_ { <. x , y >. | ( x e. f /\ y e. f ) }
11		df-xp 5120	. . . . . . . 8 |- ( f X. f ) = { <. x , y >. | ( x e. f /\ y e. f ) }
12	10, 11	sseqtr4i 3638	. . . . . . 7 |- { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } C_ ( f X. f )
13	4, 12	ssexi 4803	. . . . . 6 |- { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } e. _V
14	13	a1i 11	. . . . 5 |- ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } e. _V )
15		sseq2 3627	. . . . . . . 8 |- ( f = F -> ( { x , y } C_ f <-> { x , y } C_ F ) )
16	15	anbi1d 741	. . . . . . 7 |- ( f = F -> ( ( { x , y } C_ f /\ x C_ y ) <-> ( { x , y } C_ F /\ x C_ y ) ) )
17	16	opabbidv 4716	. . . . . 6 |- ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) } )
18		ipoval.l	. . . . . 6 |- .<_ = { <. x , y >. | ( { x , y } C_ F /\ x C_ y ) }
19	17, 18	syl6eqr 2674	. . . . 5 |- ( f = F -> { <. x , y >. | ( { x , y } C_ f /\ x C_ y ) } = .<_ )
20		simpl 473	. . . . . . . 8 |- ( ( f = F /\ o = .<_ ) -> f = F )
21	20	opeq2d 4409	. . . . . . 7 |- ( ( f = F /\ o = .<_ ) -> <. ( Base ` ndx ) , f >. = <. ( Base ` ndx ) , F >. )
22		simpr 477	. . . . . . . . 9 |- ( ( f = F /\ o = .<_ ) -> o = .<_ )
23	22	fveq2d 6195	. . . . . . . 8 |- ( ( f = F /\ o = .<_ ) -> (ordTop ` o ) = (ordTop ` .<_ ) )
24	23	opeq2d 4409	. . . . . . 7 |- ( ( f = F /\ o = .<_ ) -> <. (TopSet ` ndx ) , (ordTop ` o ) >. = <. (TopSet ` ndx ) , (ordTop ` .<_ ) >. )
25	21, 24	preq12d 4276	. . . . . 6 |- ( ( f = F /\ o = .<_ ) -> { <. ( Base ` ndx ) , f >. , <. (TopSet ` ndx ) , (ordTop ` o ) >. } = { <. ( Base ` ndx ) , F >. , <. (TopSet ` ndx ) , (ordTop ` .<_ ) >. } )
26	22	opeq2d 4409	. . . . . . 7 |- ( ( f = F /\ o = .<_ ) -> <. ( le ` ndx ) , o >. = <. ( le ` ndx ) , .<_ >. )
27		id 22	. . . . . . . . . 10 |- ( f = F -> f = F )
28		rabeq 3192	. . . . . . . . . . 11 |- ( f = F -> { y e. f | ( y i^i x ) = (/) } = { y e. F | ( y i^i x ) = (/) } )
29	28	unieqd 4446	. . . . . . . . . 10 |- ( f = F -> U. { y e. f | ( y i^i x ) = (/) } = U. { y e. F | ( y i^i x ) = (/) } )
30	27, 29	mpteq12dv 4733	. . . . . . . . 9 |- ( 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 481	. . . . . . . 8 |- ( ( 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 4409	. . . . . . 7 |- ( ( 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 4276	. . . . . 6 |- ( ( 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 3768	. . . . 5 |- ( ( 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	14, 19, 34	csbied2 3561	. . . 4 |- ( 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 17152	. . . 4 |- 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 4909	. . . . 5 |- { <. ( Base ` ndx ) , F >. , <. (TopSet ` ndx ) , (ordTop ` .<_ ) >. } e. _V
38		prex 4909	. . . . 5 |- { <. ( le ` ndx ) , .<_ >. , <. ( oc ` ndx ) , ( x e. F |-> U. { y e. F | ( y i^i x ) = (/) } ) >. } e. _V
39	37, 38	unex 6956	. . . 4 |- ( { <. ( 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 6282	. . 3 |- ( 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	2, 40	syl5eq 2668	. 2 |- ( 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	1, 41	syl 17	1 |- ( 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 ) = (/) } ) >. } ) )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   {crab 2916   _Vcvv 3200   [_csb 3533   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {cpr 4179   <.cop 4183   U.cuni 4436   {copab 4712   |-> cmpt 4729   X. cxp 5112   ` cfv 5888   ndxcnx 15854   Basecbs 15857  TopSetcts 15947   lecple 15948   occoc 15949  ordTopcordt 16159  toInccipo 17151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fv 5896  df-ipo 17152

This theorem is referenced by:  ipobas  17155  ipolerval  17156  ipotset  17157