Definition df-ipo 17762

Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 17765, ipolerval 17766, and ipole 17768 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

Step	Hyp	Ref	Expression
1		cipo 17761	. 2 class toInc
2		vf	. . 3 setvar 𝑓
3		cvv 3494	. . 3 class V
4		vo	. . . 4 setvar 𝑜
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1536	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1536	. . . . . . . 8 class 𝑦
9	6, 8	cpr 4569	. . . . . . 7 class {𝑥, 𝑦}
10	2	cv 1536	. . . . . . 7 class 𝑓
11	9, 10	wss 3936	. . . . . 6 wff {𝑥, 𝑦} ⊆ 𝑓
12	6, 8	wss 3936	. . . . . 6 wff 𝑥 ⊆ 𝑦
13	11, 12	wa 398	. . . . 5 wff ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)
14	13, 5, 7	copab 5128	. . . 4 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)}
15		cnx 16480	. . . . . . . 8 class ndx
16		cbs 16483	. . . . . . . 8 class Base
17	15, 16	cfv 6355	. . . . . . 7 class (Base‘ndx)
18	17, 10	cop 4573	. . . . . 6 class ⟨(Base‘ndx), 𝑓⟩
19		cts 16571	. . . . . . . 8 class TopSet
20	15, 19	cfv 6355	. . . . . . 7 class (TopSet‘ndx)
21	4	cv 1536	. . . . . . . 8 class 𝑜
22		cordt 16772	. . . . . . . 8 class ordTop
23	21, 22	cfv 6355	. . . . . . 7 class (ordTop‘𝑜)
24	20, 23	cop 4573	. . . . . 6 class ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩
25	18, 24	cpr 4569	. . . . 5 class {⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩}
26		cple 16572	. . . . . . . 8 class le
27	15, 26	cfv 6355	. . . . . . 7 class (le‘ndx)
28	27, 21	cop 4573	. . . . . 6 class ⟨(le‘ndx), 𝑜⟩
29		coc 16573	. . . . . . . 8 class oc
30	15, 29	cfv 6355	. . . . . . 7 class (oc‘ndx)
31	8, 6	cin 3935	. . . . . . . . . . 11 class (𝑦 ∩ 𝑥)
32		c0 4291	. . . . . . . . . . 11 class ∅
33	31, 32	wceq 1537	. . . . . . . . . 10 wff (𝑦 ∩ 𝑥) = ∅
34	33, 7, 10	crab 3142	. . . . . . . . 9 class {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅}
35	34	cuni 4838	. . . . . . . 8 class ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅}
36	5, 10, 35	cmpt 5146	. . . . . . 7 class (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})
37	30, 36	cop 4573	. . . . . 6 class ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩
38	28, 37	cpr 4569	. . . . 5 class {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}
39	25, 38	cun 3934	. . . 4 class ({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩})
40	4, 14, 39	csb 3883	. . 3 class ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩})
41	2, 3, 40	cmpt 5146	. 2 class (𝑓 ∈ V ↦ ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))
42	1, 41	wceq 1537	1 wff toInc = (𝑓 ∈ V ↦ ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))

This definition is referenced by:  ipoval  17764