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

Definition df-ipo 17467
Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 17470, ipolerval 17471, and ipole 17473 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 = (𝑓 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)} / 𝑜({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩}))
Distinct variable group:   𝑓,𝑜,𝑥,𝑦

Detailed syntax breakdown of Definition df-ipo
StepHypRef Expression
1 cipo 17466 . 2 class toInc
2 vf . . 3 setvar 𝑓
3 cvv 3385 . . 3 class V
4 vo . . . 4 setvar 𝑜
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1652 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1652 . . . . . . . 8 class 𝑦
96, 8cpr 4370 . . . . . . 7 class {𝑥, 𝑦}
102cv 1652 . . . . . . 7 class 𝑓
119, 10wss 3769 . . . . . 6 wff {𝑥, 𝑦} ⊆ 𝑓
126, 8wss 3769 . . . . . 6 wff 𝑥𝑦
1311, 12wa 385 . . . . 5 wff ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)
1413, 5, 7copab 4905 . . . 4 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)}
15 cnx 16181 . . . . . . . 8 class ndx
16 cbs 16184 . . . . . . . 8 class Base
1715, 16cfv 6101 . . . . . . 7 class (Base‘ndx)
1817, 10cop 4374 . . . . . 6 class ⟨(Base‘ndx), 𝑓
19 cts 16273 . . . . . . . 8 class TopSet
2015, 19cfv 6101 . . . . . . 7 class (TopSet‘ndx)
214cv 1652 . . . . . . . 8 class 𝑜
22 cordt 16474 . . . . . . . 8 class ordTop
2321, 22cfv 6101 . . . . . . 7 class (ordTop‘𝑜)
2420, 23cop 4374 . . . . . 6 class ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩
2518, 24cpr 4370 . . . . 5 class {⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩}
26 cple 16274 . . . . . . . 8 class le
2715, 26cfv 6101 . . . . . . 7 class (le‘ndx)
2827, 21cop 4374 . . . . . 6 class ⟨(le‘ndx), 𝑜
29 coc 16275 . . . . . . . 8 class oc
3015, 29cfv 6101 . . . . . . 7 class (oc‘ndx)
318, 6cin 3768 . . . . . . . . . . 11 class (𝑦𝑥)
32 c0 4115 . . . . . . . . . . 11 class
3331, 32wceq 1653 . . . . . . . . . 10 wff (𝑦𝑥) = ∅
3433, 7, 10crab 3093 . . . . . . . . 9 class {𝑦𝑓 ∣ (𝑦𝑥) = ∅}
3534cuni 4628 . . . . . . . 8 class {𝑦𝑓 ∣ (𝑦𝑥) = ∅}
365, 10, 35cmpt 4922 . . . . . . 7 class (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})
3730, 36cop 4374 . . . . . 6 class ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩
3828, 37cpr 4370 . . . . 5 class {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩}
3925, 38cun 3767 . . . 4 class ({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩})
404, 14, 39csb 3728 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)} / 𝑜({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩})
412, 3, 40cmpt 4922 . 2 class (𝑓 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)} / 𝑜({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩}))
421, 41wceq 1653 1 wff toInc = (𝑓 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)} / 𝑜({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩}))
Colors of variables: wff setvar class
This definition is referenced by:  ipoval  17469
  Copyright terms: Public domain W3C validator