Theorem fncvm

Description: Lemma for covering maps. (Contributed by Mario Carneiro, 13-Feb-2015)

	Ref	Expression
Assertion	fncvm	⊢ CovMap Fn ( Top × Top )

Proof

Step	Hyp	Ref	Expression
1		df-cvm	⊢ CovMap = ( 𝑐 ∈ Top , 𝑗 ∈ Top ↦ { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) } )
2		ovex	⊢ ( 𝑐 Cn 𝑗 ) ∈ V
3	2	rabex	⊢ { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) } ∈ V
4	1 3	fnmpoi	⊢ CovMap Fn ( Top × Top )