Metamath Proof Explorer

Theorem istmd

Description: The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015)

Ref Expression
Hypotheses istmd.1 ⊢ 𝐹 = ( +𝑓 ‘ 𝐺 )
istmd.2 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
Assertion istmd ( 𝐺 ∈ TopMnd ↔ ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 istmd.1 ⊢ 𝐹 = ( +𝑓 ‘ 𝐺 )
2 istmd.2 ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 elin ⊢ ( 𝐺 ∈ ( Mnd ∩ TopSp ) ↔ ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ) )
4 3 anbi1i ⊢ ( ( 𝐺 ∈ ( Mnd ∩ TopSp ) ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) ↔ ( ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ) ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )
5 fvexd ⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) ∈ V )
6 simpl ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → 𝑓 = 𝐺 )
7 6 fveq2d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( +𝑓 ‘ 𝑓 ) = ( +𝑓 ‘ 𝐺 ) )
8 7 1 eqtr4di ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( +𝑓 ‘ 𝑓 ) = 𝐹 )
9 id ⊢ ( 𝑗 = ( TopOpen ‘ 𝑓 ) → 𝑗 = ( TopOpen ‘ 𝑓 ) )
10 fveq2 ⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) = ( TopOpen ‘ 𝐺 ) )
11 10 2 eqtr4di ⊢ ( 𝑓 = 𝐺 → ( TopOpen ‘ 𝑓 ) = 𝐽 )
12 9 11 sylan9eqr ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → 𝑗 = 𝐽 )
13 12 12 oveq12d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( 𝑗 ×t 𝑗 ) = ( 𝐽 ×t 𝐽 ) )
14 13 12 oveq12d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) = ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
15 8 14 eleq12d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑗 = ( TopOpen ‘ 𝑓 ) ) → ( ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) ↔ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )
16 5 15 sbcied ⊢ ( 𝑓 = 𝐺 → ( [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) ↔ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )
17 df-tmd ⊢ TopMnd = { 𝑓 ∈ ( Mnd ∩ TopSp ) ∣ [ ( TopOpen ‘ 𝑓 ) / 𝑗 ] ( +𝑓 ‘ 𝑓 ) ∈ ( ( 𝑗 ×t 𝑗 ) Cn 𝑗 ) }
18 16 17 elrab2 ⊢ ( 𝐺 ∈ TopMnd ↔ ( 𝐺 ∈ ( Mnd ∩ TopSp ) ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )
19 df-3an ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) ↔ ( ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ) ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )
20 4 18 19 3bitr4i ⊢ ( 𝐺 ∈ TopMnd ↔ ( 𝐺 ∈ Mnd ∧ 𝐺 ∈ TopSp ∧ 𝐹 ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) ) )