Definition df-ipo

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

	Ref	Expression
Assertion	df-ipo	⊢ toInc = ( 𝑓 ∈ V ↦ ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cipo	⊢ toInc
1		vf	⊢ 𝑓
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		vy	⊢ 𝑦
5	3	cv	⊢ 𝑥
6	4	cv	⊢ 𝑦
7	5 6	cpr	⊢ { 𝑥 , 𝑦 }
8	1	cv	⊢ 𝑓
9	7 8	wss	⊢ { 𝑥 , 𝑦 } ⊆ 𝑓
10	5 6	wss	⊢ 𝑥 ⊆ 𝑦
11	9 10	wa	⊢ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 )
12	11 3 4	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) }
13		vo	⊢ 𝑜
14		cbs	⊢ Base
15		cnx	⊢ ndx
16	15 14	cfv	⊢ ( Base ‘ ndx )
17	16 8	cop	⊢ ⟨ ( Base ‘ ndx ) , 𝑓 ⟩
18		cts	⊢ TopSet
19	15 18	cfv	⊢ ( TopSet ‘ ndx )
20		cordt	⊢ ordTop
21	13	cv	⊢ 𝑜
22	21 20	cfv	⊢ ( ordTop ‘ 𝑜 )
23	19 22	cop	⊢ ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩
24	17 23	cpr	⊢ { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ }
25		cple	⊢ le
26	15 25	cfv	⊢ ( le ‘ ndx )
27	26 21	cop	⊢ ⟨ ( le ‘ ndx ) , 𝑜 ⟩
28		coc	⊢ oc
29	15 28	cfv	⊢ ( oc ‘ ndx )
30	6 5	cin	⊢ ( 𝑦 ∩ 𝑥 )
31		c0	⊢ ∅
32	30 31	wceq	⊢ ( 𝑦 ∩ 𝑥 ) = ∅
33	32 4 8	crab	⊢ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ }
34	33	cuni	⊢ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ }
35	3 8 34	cmpt	⊢ ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } )
36	29 35	cop	⊢ ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩
37	27 36	cpr	⊢ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ }
38	24 37	cun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
39	13 12 38	csb	⊢ ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
40	1 2 39	cmpt	⊢ ( 𝑓 ∈ V ↦ ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
41	0 40	wceq	⊢ toInc = ( 𝑓 ∈ V ↦ ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )