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 ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) 〉 } ) ) |
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 ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) 〉 } ) ) |