Theorem ipotset

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

	Ref	Expression
Hypotheses	ipoval.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
	ipole.l	⊢ ≤ = ( le ‘ 𝐼 )
Assertion	ipotset	⊢ ( 𝐹 ∈ 𝑉 → ( ordTop ‘ ≤ ) = ( TopSet ‘ 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipole.l	⊢ ≤ = ( le ‘ 𝐼 )
3		fvex	⊢ ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ∈ V
4		ipostr	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) Struct ⟨ 1 , ; 1 1 ⟩
5		tsetid	⊢ TopSet = Slot ( TopSet ‘ ndx )
6		snsspr2	⊢ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ }
7		ssun1	⊢ { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
8	6 7	sstri	⊢ { ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ⊆ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } )
9	4 5 8	strfv	⊢ ( ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ∈ V → ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
10	3 9	ax-mp	⊢ ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
11	1	ipolerval	⊢ ( 𝐹 ∈ 𝑉 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = ( le ‘ 𝐼 ) )
12	2 11	eqtr4id	⊢ ( 𝐹 ∈ 𝑉 → ≤ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } )
13	12	fveq2d	⊢ ( 𝐹 ∈ 𝑉 → ( ordTop ‘ ≤ ) = ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) )
14		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) }
15	1 14	ipoval	⊢ ( 𝐹 ∈ 𝑉 → 𝐼 = ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) )
16	15	fveq2d	⊢ ( 𝐹 ∈ 𝑉 → ( TopSet ‘ 𝐼 ) = ( TopSet ‘ ( { ⟨ ( Base ‘ ndx ) , 𝐹 ⟩ , ⟨ ( TopSet ‘ ndx ) , ( ordTop ‘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ) ⟩ } ∪ { ⟨ ( le ‘ ndx ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐹 ∧ 𝑥 ⊆ 𝑦 ) } ⟩ , ⟨ ( oc ‘ ndx ) , ( 𝑥 ∈ 𝐹 ↦ ∪ { 𝑦 ∈ 𝐹 ∣ ( 𝑦 ∩ 𝑥 ) = ∅ } ) ⟩ } ) ) )
17	10 13 16	3eqtr4a	⊢ ( 𝐹 ∈ 𝑉 → ( ordTop ‘ ≤ ) = ( TopSet ‘ 𝐼 ) )