Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ipoval Structured version   Unicode version

Theorem ipoval 16405
 Description: Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015.)
Hypotheses
Ref Expression
ipoval.i toInc
ipoval.l
Assertion
Ref Expression
ipoval TopSet ordTop
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem ipoval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3094 . 2
2 ipoval.i . . 3 toInc
3 vex 3088 . . . . . . . 8
43, 3xpex 6615 . . . . . . 7
5 simpl 459 . . . . . . . . . 10
6 vex 3088 . . . . . . . . . . 11
7 vex 3088 . . . . . . . . . . 11
86, 7prss 4160 . . . . . . . . . 10
95, 8sylibr 216 . . . . . . . . 9
109ssopab2i 4754 . . . . . . . 8
11 df-xp 4865 . . . . . . . 8
1210, 11sseqtr4i 3503 . . . . . . 7
134, 12ssexi 4575 . . . . . 6
1413a1i 11 . . . . 5
15 sseq2 3492 . . . . . . . 8
1615anbi1d 710 . . . . . . 7
1716opabbidv 4493 . . . . . 6
18 ipoval.l . . . . . 6
1917, 18syl6eqr 2482 . . . . 5
20 simpl 459 . . . . . . . 8
2120opeq2d 4200 . . . . . . 7
22 simpr 463 . . . . . . . . 9
2322fveq2d 5891 . . . . . . . 8 ordTop ordTop
2423opeq2d 4200 . . . . . . 7 TopSet ordTop TopSet ordTop
2521, 24preq12d 4093 . . . . . 6 TopSet ordTop TopSet ordTop
2622opeq2d 4200 . . . . . . 7
27 id 23 . . . . . . . . . 10
28 rabeq 3078 . . . . . . . . . . 11
2928unieqd 4235 . . . . . . . . . 10
3027, 29mpteq12dv 4508 . . . . . . . . 9
3130adantr 467 . . . . . . . 8
3231opeq2d 4200 . . . . . . 7
3326, 32preq12d 4093 . . . . . 6
3425, 33uneq12d 3627 . . . . 5 TopSet ordTop TopSet ordTop
3514, 19, 34csbied2 3429 . . . 4 TopSet ordTop TopSet ordTop
36 df-ipo 16403 . . . 4 toInc TopSet ordTop
37 prex 4669 . . . . 5 TopSet ordTop
38 prex 4669 . . . . 5
3937, 38unex 6609 . . . 4 TopSet ordTop
4035, 36, 39fvmpt 5970 . . 3 toInc TopSet ordTop
412, 40syl5eq 2476 . 2 TopSet ordTop
421, 41syl 17 1 TopSet ordTop
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   wceq 1438   wcel 1873  crab 2780  cvv 3085  csb 3401   cun 3440   cin 3441   wss 3442  c0 3767  cpr 4006  cop 4010  cuni 4225  copab 4487   cmpt 4488   cxp 4857  cfv 5607  cnx 15123  cbs 15126  TopSetcts 15201  cple 15202  coc 15203  ordTopcordt 15402  toInccipo 16402 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-8 1875  ax-9 1877  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402  ax-sep 4552  ax-nul 4561  ax-pow 4608  ax-pr 4666  ax-un 6603 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3087  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3918  df-pw 3989  df-sn 4005  df-pr 4007  df-op 4011  df-uni 4226  df-br 4430  df-opab 4489  df-mpt 4490  df-id 4774  df-xp 4865  df-rel 4866  df-cnv 4867  df-co 4868  df-dm 4869  df-iota 5571  df-fun 5609  df-fv 5615  df-ipo 16403 This theorem is referenced by:  ipobas  16406  ipolerval  16407  ipotset  16408
 Copyright terms: Public domain W3C validator