Metamath Proof Explorer


Theorem ipotset

Description: Topology of the inclusion poset. (Contributed by Mario Carneiro, 24-Oct-2015)

Ref Expression
Hypotheses ipoval.i I = toInc F
ipole.l ˙ = I
Assertion ipotset F V ordTop ˙ = TopSet I

Proof

Step Hyp Ref Expression
1 ipoval.i I = toInc F
2 ipole.l ˙ = I
3 fvex ordTop x y | x y F x y V
4 ipostr Base ndx F TopSet ndx ordTop x y | x y F x y ndx x y | x y F x y oc ndx x F y F | y x = Struct 1 11
5 tsetid TopSet = Slot TopSet ndx
6 snsspr2 TopSet ndx ordTop x y | x y F x y Base ndx F TopSet ndx ordTop x y | x y F x y
7 ssun1 Base ndx F TopSet ndx ordTop x y | x y F x y Base ndx F TopSet ndx ordTop x y | x y F x y ndx x y | x y F x y oc ndx x F y F | y x =
8 6 7 sstri TopSet ndx ordTop x y | x y F x y Base ndx F TopSet ndx ordTop x y | x y F x y ndx x y | x y F x y oc ndx x F y F | y x =
9 4 5 8 strfv ordTop x y | x y F x y V ordTop x y | x y F x y = TopSet Base ndx F TopSet ndx ordTop x y | x y F x y ndx x y | x y F x y oc ndx x F y F | y x =
10 3 9 ax-mp ordTop x y | x y F x y = TopSet Base ndx F TopSet ndx ordTop x y | x y F x y ndx x y | x y F x y oc ndx x F y F | y x =
11 1 ipolerval F V x y | x y F x y = I
12 2 11 eqtr4id F V ˙ = x y | x y F x y
13 12 fveq2d F V ordTop ˙ = ordTop x y | x y F x y
14 eqid x y | x y F x y = x y | x y F x y
15 1 14 ipoval F V I = Base ndx F TopSet ndx ordTop x y | x y F x y ndx x y | x y F x y oc ndx x F y F | y x =
16 15 fveq2d F V TopSet I = TopSet Base ndx F TopSet ndx ordTop x y | x y F x y ndx x y | x y F x y oc ndx x F y F | y x =
17 10 13 16 3eqtr4a F V ordTop ˙ = TopSet I