Definition df-ipo 18573

Description: For any family of sets, define the poset of that family ordered by inclusion. See ipobas 18576, ipolerval 18577, and ipole 18579 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 18572	. 2 class toInc
2		vf	. . 3 setvar 𝑓
3		cvv 3480	. . 3 class V
4		vo	. . . 4 setvar 𝑜
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1539	. . . . . . . 8 class 𝑥
7		vy	. . . . . . . . 9 setvar 𝑦
8	7	cv 1539	. . . . . . . 8 class 𝑦
9	6, 8	cpr 4628	. . . . . . 7 class {𝑥, 𝑦}
10	2	cv 1539	. . . . . . 7 class 𝑓
11	9, 10	wss 3951	. . . . . 6 wff {𝑥, 𝑦} ⊆ 𝑓
12	6, 8	wss 3951	. . . . . 6 wff 𝑥 ⊆ 𝑦
13	11, 12	wa 395	. . . . 5 wff ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)
14	13, 5, 7	copab 5205	. . . 4 class {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)}
15		cnx 17230	. . . . . . . 8 class ndx
16		cbs 17247	. . . . . . . 8 class Base
17	15, 16	cfv 6561	. . . . . . 7 class (Base‘ndx)
18	17, 10	cop 4632	. . . . . 6 class ⟨(Base‘ndx), 𝑓⟩
19		cts 17303	. . . . . . . 8 class TopSet
20	15, 19	cfv 6561	. . . . . . 7 class (TopSet‘ndx)
21	4	cv 1539	. . . . . . . 8 class 𝑜
22		cordt 17544	. . . . . . . 8 class ordTop
23	21, 22	cfv 6561	. . . . . . 7 class (ordTop‘𝑜)
24	20, 23	cop 4632	. . . . . 6 class ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩
25	18, 24	cpr 4628	. . . . 5 class {⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩}
26		cple 17304	. . . . . . . 8 class le
27	15, 26	cfv 6561	. . . . . . 7 class (le‘ndx)
28	27, 21	cop 4632	. . . . . 6 class ⟨(le‘ndx), 𝑜⟩
29		coc 17305	. . . . . . . 8 class oc
30	15, 29	cfv 6561	. . . . . . 7 class (oc‘ndx)
31	8, 6	cin 3950	. . . . . . . . . . 11 class (𝑦 ∩ 𝑥)
32		c0 4333	. . . . . . . . . . 11 class ∅
33	31, 32	wceq 1540	. . . . . . . . . 10 wff (𝑦 ∩ 𝑥) = ∅
34	33, 7, 10	crab 3436	. . . . . . . . 9 class {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅}
35	34	cuni 4907	. . . . . . . 8 class ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅}
36	5, 10, 35	cmpt 5225	. . . . . . 7 class (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})
37	30, 36	cop 4632	. . . . . 6 class ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩
38	28, 37	cpr 4628	. . . . 5 class {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}
39	25, 38	cun 3949	. . . 4 class ({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩})
40	4, 14, 39	csb 3899	. . 3 class ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩})
41	2, 3, 40	cmpt 5225	. 2 class (𝑓 ∈ V ↦ ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))
42	1, 41	wceq 1540	1 wff toInc = (𝑓 ∈ V ↦ ⦋{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦)} / 𝑜⦌({⟨(Base‘ndx), 𝑓⟩, ⟨(TopSet‘ndx), (ordTop‘𝑜)⟩} ∪ {⟨(le‘ndx), 𝑜⟩, ⟨(oc‘ndx), (𝑥 ∈ 𝑓 ↦ ∪ {𝑦 ∈ 𝑓 ∣ (𝑦 ∩ 𝑥) = ∅})⟩}))

This definition is referenced by:  ipoval  18575