Theorem topclat

Description: A topology is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypothesis	topclat.i	|- I = ( toInc ` J )
Assertion	topclat	|- ( J e. Top -> I e. CLat )

Proof

Step	Hyp	Ref	Expression
1		topclat.i	|- I = ( toInc ` J )
2	1	ipobas	|- ( J e. Top -> J = ( Base ` I ) )
3		eqidd	|- ( J e. Top -> ( lub ` I ) = ( lub ` I ) )
4		eqidd	|- ( J e. Top -> ( glb ` I ) = ( glb ` I ) )
5	1	ipopos	|- I e. Poset
6	5	a1i	|- ( J e. Top -> I e. Poset )
7		uniopn	|- ( ( J e. Top /\ x C_ J ) -> U. x e. J )
8		simpl	|- ( ( J e. Top /\ x C_ J ) -> J e. Top )
9		simpr	|- ( ( J e. Top /\ x C_ J ) -> x C_ J )
10		eqidd	|- ( ( J e. Top /\ x C_ J ) -> ( lub ` I ) = ( lub ` I ) )
11		intmin	|- ( U. x e. J -> |^| { y e. J | U. x C_ y } = U. x )
12	11	eqcomd	|- ( U. x e. J -> U. x = |^| { y e. J | U. x C_ y } )
13	7 12	syl	|- ( ( J e. Top /\ x C_ J ) -> U. x = |^| { y e. J | U. x C_ y } )
14	1 8 9 10 13	ipolubdm	|- ( ( J e. Top /\ x C_ J ) -> ( x e. dom ( lub ` I ) <-> U. x e. J ) )
15	7 14	mpbird	|- ( ( J e. Top /\ x C_ J ) -> x e. dom ( lub ` I ) )
16		ssrab2	|- { y e. J | y C_ |^| x } C_ J
17		uniopn	|- ( ( J e. Top /\ { y e. J | y C_ |^| x } C_ J ) -> U. { y e. J | y C_ |^| x } e. J )
18	8 16 17	sylancl	|- ( ( J e. Top /\ x C_ J ) -> U. { y e. J | y C_ |^| x } e. J )
19		eqidd	|- ( ( J e. Top /\ x C_ J ) -> ( glb ` I ) = ( glb ` I ) )
20		eqidd	|- ( ( J e. Top /\ x C_ J ) -> U. { y e. J | y C_ |^| x } = U. { y e. J | y C_ |^| x } )
21	1 8 9 19 20	ipoglbdm	|- ( ( J e. Top /\ x C_ J ) -> ( x e. dom ( glb ` I ) <-> U. { y e. J | y C_ |^| x } e. J ) )
22	18 21	mpbird	|- ( ( J e. Top /\ x C_ J ) -> x e. dom ( glb ` I ) )
23	2 3 4 6 15 22	isclatd	|- ( J e. Top -> I e. CLat )