This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnfval

Description: The set of all continuous functions from topology J to topology K . (Contributed by NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnfval ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 Cn 𝐾 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } )

Proof

Step Hyp Ref Expression
1 df-cn ⊢ Cn = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 } )
2 1 a1i ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → Cn = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 } ) )
3 simprr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑘 = 𝐾 )
4 3 unieqd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑘 = ∪ 𝐾 )
5 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
6 5 ad2antlr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑌 = ∪ 𝐾 )
7 4 6 eqtr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑘 = 𝑌 )
8 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑗 = 𝐽 )
9 8 unieqd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑗 = ∪ 𝐽 )
10 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
11 10 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → 𝑋 = ∪ 𝐽 )
12 9 11 eqtr4d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ∪ 𝑗 = 𝑋 )
13 7 12 oveq12d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ∪ 𝑘 ↑m ∪ 𝑗 ) = ( 𝑌 ↑m 𝑋 ) )
14 8 eleq2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 ↔ ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 ) )
15 3 14 raleqbidv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → ( ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 ↔ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 ) )
16 13 15 rabeqbidv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) ) → { 𝑓 ∈ ( ∪ 𝑘 ↑m ∪ 𝑗 ) ∣ ∀ 𝑦 ∈ 𝑘 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝑗 } = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } )
17 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
18 17 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐽 ∈ Top )
19 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
20 19 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → 𝐾 ∈ Top )
21 ovex ⊢ ( 𝑌 ↑m 𝑋 ) ∈ V
22 21 rabex ⊢ { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } ∈ V
23 22 a1i ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } ∈ V )
24 2 16 18 20 23 ovmpod ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐽 Cn 𝐾 ) = { 𝑓 ∈ ( 𝑌 ↑m 𝑋 ) ∣ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝑓 “ 𝑦 ) ∈ 𝐽 } )