Theorem iscnrm3rlem6

Description: Lemma for iscnrm3rlem7 . (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Hypotheses	iscnrm3rlem4.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	iscnrm3rlem4.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
	iscnrm3rlem5.3	⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
	iscnrm3rlem6.4	⊢ ( 𝜑 → 𝑂 ⊆ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) )
Assertion	iscnrm3rlem6	⊢ ( 𝜑 → ( 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ↔ 𝑂 ∈ 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem4.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		iscnrm3rlem4.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
3		iscnrm3rlem5.3	⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
4		iscnrm3rlem6.4	⊢ ( 𝜑 → 𝑂 ⊆ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) )
5	1 2 3	iscnrm3rlem5	⊢ ( 𝜑 → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝐽 )
6		restopn2	⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝐽 ) → ( 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ↔ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) )
7	1 5 6	syl2anc	⊢ ( 𝜑 → ( 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ↔ ( 𝑂 ∈ 𝐽 ∧ 𝑂 ⊆ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) )
8	4 7	mpbiran2d	⊢ ( 𝜑 → ( 𝑂 ∈ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ↔ 𝑂 ∈ 𝐽 ) )