Theorem toplatjoin

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

	Ref	Expression
Hypotheses	toplatmeet.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
	toplatmeet.j	$$⊢\phi \to J\in \mathrm{Top}$$
	toplatmeet.a	$$⊢\phi \to A\in J$$
	toplatmeet.b	$$⊢\phi \to B\in J$$
	toplatjoin.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(I\right)$$
Assertion	toplatjoin	$$⊢\phi \to A\underset{\dot{}}{\vee }B=A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		toplatmeet.i	$$⊢I=\mathrm{toInc}\left(J\right)$$
2		toplatmeet.j	$$⊢\phi \to J\in \mathrm{Top}$$
3		toplatmeet.a	$$⊢\phi \to A\in J$$
4		toplatmeet.b	$$⊢\phi \to B\in J$$
5		toplatjoin.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(I\right)$$
6		eqid	$$⊢\mathrm{lub}\left(I\right)=\mathrm{lub}\left(I\right)$$
7	1	ipopos	$$⊢I\in \mathrm{Poset}$$
8	7	a1i	$$⊢\phi \to I\in \mathrm{Poset}$$
9	6 5 8 3 4	joinval	$$⊢\phi \to A\underset{\dot{}}{\vee }B=\mathrm{lub}\left(I\right)\left(\left\{A,B\right\}\right)$$
10	3 4	prssd	$$⊢\phi \to \left\{A,B\right\}\subseteq J$$
11	6	a1i	$$⊢\phi \to \mathrm{lub}\left(I\right)=\mathrm{lub}\left(I\right)$$
12		uniprg	$$⊢\left(A\in J\wedge B\in J\right)\to \bigcup \left\{A,B\right\}=A\cup B$$
13	3 4 12	syl2anc	$$⊢\phi \to \bigcup \left\{A,B\right\}=A\cup B$$
14		unopn	$$⊢\left(J\in \mathrm{Top}\wedge A\in J\wedge B\in J\right)\to A\cup B\in J$$
15	2 3 4 14	syl3anc	$$⊢\phi \to A\cup B\in J$$
16	13 15	eqeltrd	$$⊢\phi \to \bigcup \left\{A,B\right\}\in J$$
17		intmin	$$⊢\bigcup \left\{A,B\right\}\in J\to \bigcap \left\{x\in J|\bigcup \left\{A,B\right\}\subseteq x\right\}=\bigcup \left\{A,B\right\}$$
18	16 17	syl	$$⊢\phi \to \bigcap \left\{x\in J|\bigcup \left\{A,B\right\}\subseteq x\right\}=\bigcup \left\{A,B\right\}$$
19	18 13	eqtr2d	$$⊢\phi \to A\cup B=\bigcap \left\{x\in J|\bigcup \left\{A,B\right\}\subseteq x\right\}$$
20	1 2 10 11 19 15	ipolub	$$⊢\phi \to \mathrm{lub}\left(I\right)\left(\left\{A,B\right\}\right)=A\cup B$$
21	9 20	eqtrd	$$⊢\phi \to A\underset{\dot{}}{\vee }B=A\cup B$$