Theorem toplatjoin

Description: Joins in a topology are realized by unions. (Contributed by Zhi Wang, 30-Sep-2024)

	Ref	Expression
Hypotheses	toplatmeet.i	|- I = ( toInc ` J )
	toplatmeet.j	|- ( ph -> J e. Top )
	toplatmeet.a	|- ( ph -> A e. J )
	toplatmeet.b	|- ( ph -> B e. J )
	toplatjoin.j	|- .\/ = ( join ` I )
Assertion	toplatjoin	|- ( ph -> ( A .\/ B ) = ( A u. B ) )

Proof

Step	Hyp	Ref	Expression
1		toplatmeet.i	|- I = ( toInc ` J )
2		toplatmeet.j	|- ( ph -> J e. Top )
3		toplatmeet.a	|- ( ph -> A e. J )
4		toplatmeet.b	|- ( ph -> B e. J )
5		toplatjoin.j	|- .\/ = ( join ` I )
6		eqid	|- ( lub ` I ) = ( lub ` I )
7	1	ipopos	|- I e. Poset
8	7	a1i	|- ( ph -> I e. Poset )
9	6 5 8 3 4	joinval	|- ( ph -> ( A .\/ B ) = ( ( lub ` I ) ` { A , B } ) )
10	3 4	prssd	|- ( ph -> { A , B } C_ J )
11	6	a1i	|- ( ph -> ( lub ` I ) = ( lub ` I ) )
12		uniprg	|- ( ( A e. J /\ B e. J ) -> U. { A , B } = ( A u. B ) )
13	3 4 12	syl2anc	|- ( ph -> U. { A , B } = ( A u. B ) )
14		unopn	|- ( ( J e. Top /\ A e. J /\ B e. J ) -> ( A u. B ) e. J )
15	2 3 4 14	syl3anc	|- ( ph -> ( A u. B ) e. J )
16	13 15	eqeltrd	|- ( ph -> U. { A , B } e. J )
17		intmin	|- ( U. { A , B } e. J -> |^| { x e. J | U. { A , B } C_ x } = U. { A , B } )
18	16 17	syl	|- ( ph -> |^| { x e. J | U. { A , B } C_ x } = U. { A , B } )
19	18 13	eqtr2d	|- ( ph -> ( A u. B ) = |^| { x e. J | U. { A , B } C_ x } )
20	1 2 10 11 19 15	ipolub	|- ( ph -> ( ( lub ` I ) ` { A , B } ) = ( A u. B ) )
21	9 20	eqtrd	|- ( ph -> ( A .\/ B ) = ( A u. B ) )