Theorem toplatjoin

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

	Ref	Expression
Hypotheses	toplatmeet.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
	toplatmeet.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
	toplatmeet.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
	toplatmeet.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
	toplatjoin.j	⊢ ∨ = ( join ‘ 𝐼 )
Assertion	toplatjoin	⊢ ( 𝜑 → ( 𝐴 ∨ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		toplatmeet.i	⊢ 𝐼 = ( toInc ‘ 𝐽 )
2		toplatmeet.j	⊢ ( 𝜑 → 𝐽 ∈ Top )
3		toplatmeet.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
4		toplatmeet.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
5		toplatjoin.j	⊢ ∨ = ( join ‘ 𝐼 )
6		eqid	⊢ ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 )
7	1	ipopos	⊢ 𝐼 ∈ Poset
8	7	a1i	⊢ ( 𝜑 → 𝐼 ∈ Poset )
9	6 5 8 3 4	joinval	⊢ ( 𝜑 → ( 𝐴 ∨ 𝐵 ) = ( ( lub ‘ 𝐼 ) ‘ { 𝐴 , 𝐵 } ) )
10	3 4	prssd	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ⊆ 𝐽 )
11	6	a1i	⊢ ( 𝜑 → ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 ) )
12		uniprg	⊢ ( ( 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
13	3 4 12	syl2anc	⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
14		unopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽 ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝐽 )
15	2 3 4 14	syl3anc	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ 𝐽 )
16	13 15	eqeltrd	⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } ∈ 𝐽 )
17		intmin	⊢ ( ∪ { 𝐴 , 𝐵 } ∈ 𝐽 → ∩ { 𝑥 ∈ 𝐽 ∣ ∪ { 𝐴 , 𝐵 } ⊆ 𝑥 } = ∪ { 𝐴 , 𝐵 } )
18	16 17	syl	⊢ ( 𝜑 → ∩ { 𝑥 ∈ 𝐽 ∣ ∪ { 𝐴 , 𝐵 } ⊆ 𝑥 } = ∪ { 𝐴 , 𝐵 } )
19	18 13	eqtr2d	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = ∩ { 𝑥 ∈ 𝐽 ∣ ∪ { 𝐴 , 𝐵 } ⊆ 𝑥 } )
20	1 2 10 11 19 15	ipolub	⊢ ( 𝜑 → ( ( lub ‘ 𝐼 ) ‘ { 𝐴 , 𝐵 } ) = ( 𝐴 ∪ 𝐵 ) )
21	9 20	eqtrd	⊢ ( 𝜑 → ( 𝐴 ∨ 𝐵 ) = ( 𝐴 ∪ 𝐵 ) )