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 17073
Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 17076, ipolerval 17077, and ipole 17079 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 17072 . 2 class toInc
2 vf . . 3 setvar 𝑓
3 cvv 3186 . . 3 class V
4 vo . . . 4 setvar 𝑜
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1479 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1479 . . . . . . . 8 class 𝑦
96, 8cpr 4150 . . . . . . 7 class {𝑥, 𝑦}
102cv 1479 . . . . . . 7 class 𝑓
119, 10wss 3555 . . . . . 6 wff {𝑥, 𝑦} ⊆ 𝑓
126, 8wss 3555 . . . . . 6 wff 𝑥𝑦
1311, 12wa 384 . . . . 5 wff ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)
1413, 5, 7copab 4672 . . . 4 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)}
15 cnx 15778 . . . . . . . 8 class ndx
16 cbs 15781 . . . . . . . 8 class Base
1715, 16cfv 5847 . . . . . . 7 class (Base‘ndx)
1817, 10cop 4154 . . . . . 6 class ⟨(Base‘ndx), 𝑓
19 cts 15868 . . . . . . . 8 class TopSet
2015, 19cfv 5847 . . . . . . 7 class (TopSet‘ndx)
214cv 1479 . . . . . . . 8 class 𝑜
22 cordt 16080 . . . . . . . 8 class ordTop
2321, 22cfv 5847 . . . . . . 7 class (ordTop‘𝑜)
2420, 23cop 4154 . . . . . 6 class ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩
2518, 24cpr 4150 . . . . 5 class {⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩}
26 cple 15869 . . . . . . . 8 class le
2715, 26cfv 5847 . . . . . . 7 class (le‘ndx)
2827, 21cop 4154 . . . . . 6 class ⟨(le‘ndx), 𝑜
29 coc 15870 . . . . . . . 8 class oc
3015, 29cfv 5847 . . . . . . 7 class (oc‘ndx)
318, 6cin 3554 . . . . . . . . . . 11 class (𝑦𝑥)
32 c0 3891 . . . . . . . . . . 11 class
3331, 32wceq 1480 . . . . . . . . . 10 wff (𝑦𝑥) = ∅
3433, 7, 10crab 2911 . . . . . . . . 9 class {𝑦𝑓 ∣ (𝑦𝑥) = ∅}
3534cuni 4402 . . . . . . . 8 class {𝑦𝑓 ∣ (𝑦𝑥) = ∅}
365, 10, 35cmpt 4673 . . . . . . 7 class (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})
3730, 36cop 4154 . . . . . 6 class ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩
3828, 37cpr 4150 . . . . 5 class {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩}
3925, 38cun 3553 . . . 4 class ({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩})
404, 14, 39csb 3514 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)} / 𝑜({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩})
412, 3, 40cmpt 4673 . 2 class (𝑓 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓𝑥𝑦)} / 𝑜({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥𝑓 {𝑦𝑓 ∣ (𝑦𝑥) = ∅})⟩}))
421, 41wceq 1480 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  17075
  Copyright terms: Public domain W3C validator