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

Definition df-ipo 14583
 Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 14586, ipolerval 14587, and ipole 14589 for its contract. EDITORIAL: I'm not thrilled with the name. Any suggestions? (Contributed by Stefan O'Rear, 30-Jan-2015.) (New usage is discouraged.)
Assertion
Ref Expression
df-ipo toInc TopSet ordTop
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-ipo
StepHypRef Expression
1 cipo 14582 . 2 toInc
2 vf . . 3
3 cvv 2958 . . 3
4 vo . . . 4
5 vx . . . . . . . . 9
65cv 1652 . . . . . . . 8
7 vy . . . . . . . . 9
87cv 1652 . . . . . . . 8
96, 8cpr 3817 . . . . . . 7
102cv 1652 . . . . . . 7
119, 10wss 3322 . . . . . 6
126, 8wss 3322 . . . . . 6
1311, 12wa 360 . . . . 5
1413, 5, 7copab 4268 . . . 4
15 cnx 13471 . . . . . . . 8
16 cbs 13474 . . . . . . . 8
1715, 16cfv 5457 . . . . . . 7
1817, 10cop 3819 . . . . . 6
19 cts 13540 . . . . . . . 8 TopSet
2015, 19cfv 5457 . . . . . . 7 TopSet
214cv 1652 . . . . . . . 8
22 cordt 13726 . . . . . . . 8 ordTop
2321, 22cfv 5457 . . . . . . 7 ordTop
2420, 23cop 3819 . . . . . 6 TopSet ordTop
2518, 24cpr 3817 . . . . 5 TopSet ordTop
26 cple 13541 . . . . . . . 8
2715, 26cfv 5457 . . . . . . 7
2827, 21cop 3819 . . . . . 6
29 coc 13542 . . . . . . . 8
3015, 29cfv 5457 . . . . . . 7
318, 6cin 3321 . . . . . . . . . . 11
32 c0 3630 . . . . . . . . . . 11
3331, 32wceq 1653 . . . . . . . . . 10
3433, 7, 10crab 2711 . . . . . . . . 9
3534cuni 4017 . . . . . . . 8
365, 10, 35cmpt 4269 . . . . . . 7
3730, 36cop 3819 . . . . . 6
3828, 37cpr 3817 . . . . 5
3925, 38cun 3320 . . . 4 TopSet ordTop
404, 14, 39csb 3253 . . 3 TopSet ordTop
412, 3, 40cmpt 4269 . 2 TopSet ordTop
421, 41wceq 1653 1 toInc TopSet ordTop
 Colors of variables: wff set class This definition is referenced by:  ipoval  14585
 Copyright terms: Public domain W3C validator