This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipoval

Description: Value of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Hypotheses ipoval.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
ipoval.l ⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
Assertion ipoval ( 𝐹 ∈ 𝑉 → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )

Proof

Step Hyp Ref Expression
1 ipoval.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
2 ipoval.l ⊢ ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
3 elex ⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
4 vex ⊢ 𝑓 ∈ V
5 4 4 xpex ⊢ ( 𝑓 × 𝑓 ) ∈ V
6 simpl ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) → { 𝑥 , 𝑦 } ⊆ 𝑓 )
7 vex ⊢ 𝑥 ∈ V
8 vex ⊢ 𝑦 ∈ V
9 7 8 prss ⊢ ( ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝑓 )
10 6 9 sylibr ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) )
11 10 ssopab2i ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) }
12 df-xp ⊢ ( 𝑓 × 𝑓 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝑓 ∧ 𝑦 ∈ 𝑓 ) }
13 11 12 sseqtrri ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ ( 𝑓 × 𝑓 )
14 5 13 ssexi ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V
15 14 a1i ⊢ ( 𝑓 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V )
16 sseq2 ⊢ ( 𝑓 = 𝐹 → ( { 𝑥 , 𝑦 } ⊆ 𝑓 ↔ { 𝑥 , 𝑦 } ⊆ 𝐹 ) )
17 16 anbi1d ⊢ ( 𝑓 = 𝐹 → ( ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) ) )
18 17 opabbidv ⊢ ( 𝑓 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } )
19 18 2 eqtr4di ⊢ ( 𝑓 = 𝐹 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } = ≤ )
20 simpl ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → 𝑓 = 𝐹 )
21 20 opeq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ = ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ )
22 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → 𝑜 = ≤ )
23 22 fveq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ( ordTop ‘ 𝑜 ) = ( ordTop ‘ ≤ ) )
24 23 opeq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ )
25 21 24 preq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } )
26 22 opeq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( le ‘ ndx ) , 𝑜 ⟩ = ⟨ ( le ‘ ndx ) , ≤ ⟩ )
27 id ⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
28 rabeq ⊢ ( 𝑓 = 𝐹 → { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } = { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } )
29 28 unieqd ⊢ ( 𝑓 = 𝐹 → ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } = ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } )
30 27 29 mpteq12dv ⊢ ( 𝑓 = 𝐹 → ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) = ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) )
31 30 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) = ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) )
32 31 opeq2d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ = ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ )
33 26 32 preq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } = { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
34 25 33 uneq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑜 = ≤ ) → ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
35 15 19 34 csbied2 ⊢ ( 𝑓 = 𝐹 → ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
36 df-ipo ⊢ toInc = ( 𝑓 ∈ V ↦ ⦋ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑓 ∧ 𝑥 ⊆ 𝑦 ) } / 𝑜 ⦌ ( { ⟨ ( Base ‘ ndx ) , 𝑓 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ 𝑜 ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , 𝑜 ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝑓 ↦ ∪ { 𝑦 ∈ 𝑓 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
37 prex ⊢ { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∈ V
38 prex ⊢ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ∈ V
39 37 38 unex ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ∈ V
40 35 36 39 fvmpt ⊢ ( 𝐹 ∈ V → ( toInc ‘ 𝐹 ) = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
41 1 40 eqtrid ⊢ ( 𝐹 ∈ V → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
42 3 41 syl ⊢ ( 𝐹 ∈ 𝑉 → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ ≤ ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )