Metamath Proof Explorer


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 ) , ( 𝑥𝑓 { 𝑦𝑓 ∣ ( 𝑦𝑥 ) = ∅ } ) ⟩ } ) )