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

Metamath Proof Explorer

Theorem ipolerval

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

Ref Expression
Hypothesis ipoval.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
Assertion ipolerval ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )

Proof

Step Hyp Ref Expression
1 ipoval.i ⊢ 𝐼 = ( toInc ‘ 𝐹 )
2 simpl ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) → { 𝑥 , 𝑦 } ⊆ 𝐹 )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 3 4 prss ⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐹 )
6 2 5 sylibr ⊢ ( ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) )
7 6 ssopab2i ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) }
8 df-xp ⊢ ( 𝐹 × 𝐹 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) }
9 7 8 sseqtrri ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ ( 𝐹 × 𝐹 )
10 sqxpexg ⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 × 𝐹 ) ∈ V )
11 ssexg ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⊆ ( 𝐹 × 𝐹 ) ∧ ( 𝐹 × 𝐹 ) ∈ V ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V )
12 9 10 11 sylancr ⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V )
13 ipostr ⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) Struct ⟨ 1 , 1 1 ⟩
14 pleid ⊢ le = Slot ( le ‘ ndx )
15 snsspr1 ⊢ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ } ⊆ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ }
16 ssun2 ⊢ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
17 15 16 sstri ⊢ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
18 13 14 17 strfv ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ∈ V → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
19 12 18 syl ⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
20 eqid ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
21 1 20 ipoval ⊢ ( 𝐹 ∈ 𝑉 → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
22 21 fveq2d ⊢ ( 𝐹 ∈ 𝑉 → ( le ‘ 𝐼 ) = ( le ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
23 19 22 eqtr4d ⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )