Metamath Proof Explorer

Theorem iscvm

Description: The property of being a covering map. (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypotheses iscvm.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
iscvm.2 ⊢ 𝑋 = ∪ 𝐽
Assertion iscvm ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 iscvm.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 iscvm.2 ⊢ 𝑋 = ∪ 𝐽
3 anass ⊢ ( ( ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) ) )
4 df-3an ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) )
5 4 anbi1i ⊢ ( ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) ↔ ( ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )
6 df-cvm ⊢ CovMap = ( 𝑐 ∈ Top , 𝑗 ∈ Top ↦ { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) } )
7 6 elmpocl ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) )
8 oveq12 ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( 𝑐 Cn 𝑗 ) = ( 𝐶 Cn 𝐽 ) )
9 simpr ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → 𝑗 = 𝐽 )
10 9 unieqd ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ∪ 𝑗 = ∪ 𝐽 )
11 10 2 eqtr4di ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ∪ 𝑗 = 𝑋 )
12 simpl ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → 𝑐 = 𝐶 )
13 12 pweqd ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → 𝒫 𝑐 = 𝒫 𝐶 )
14 13 difeq1d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( 𝒫 𝑐 ∖ { ∅ } ) = ( 𝒫 𝐶 ∖ { ∅ } ) )
15 oveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ↾t 𝑢 ) = ( 𝐶 ↾t 𝑢 ) )
16 oveq1 ⊢ ( 𝑗 = 𝐽 → ( 𝑗 ↾t 𝑘 ) = ( 𝐽 ↾t 𝑘 ) )
17 15 16 oveqan12d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) = ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) )
18 17 eleq2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ↔ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) )
19 18 anbi2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ↔ ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
20 19 ralbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ↔ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
21 20 anbi2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ↔ ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) )
22 14 21 rexeqbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ↔ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) )
23 22 anbi2d ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) ↔ ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
24 9 23 rexeqbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) ↔ ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
25 11 24 raleqbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → ( ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
26 8 25 rabeqbidv ⊢ ( ( 𝑐 = 𝐶 ∧ 𝑗 = 𝐽 ) → { 𝑓 ∈ ( 𝑐 Cn 𝑗 ) ∣ ∀ 𝑥 ∈ ∪ 𝑗 ∃ 𝑘 ∈ 𝑗 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝑐 ↾t 𝑢 ) Homeo ( 𝑗 ↾t 𝑘 ) ) ) ) ) } = { 𝑓 ∈ ( 𝐶 Cn 𝐽 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) } )
27 ovex ⊢ ( 𝐶 Cn 𝐽 ) ∈ V
28 27 rabex ⊢ { 𝑓 ∈ ( 𝐶 Cn 𝐽 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) } ∈ V
29 26 6 28 ovmpoa ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐶 CovMap 𝐽 ) = { 𝑓 ∈ ( 𝐶 Cn 𝐽 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) } )
30 29 eleq2d ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝐶 Cn 𝐽 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) } ) )
31 id ⊢ ( 𝑘 ∈ 𝐽 → 𝑘 ∈ 𝐽 )
32 pwexg ⊢ ( 𝐶 ∈ Top → 𝒫 𝐶 ∈ V )
33 32 adantr ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → 𝒫 𝐶 ∈ V )
34 difexg ⊢ ( 𝒫 𝐶 ∈ V → ( 𝒫 𝐶 ∖ { ∅ } ) ∈ V )
35 rabexg ⊢ ( ( 𝒫 𝐶 ∖ { ∅ } ) ∈ V → { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ∈ V )
36 33 34 35 3syl ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ∈ V )
37 1 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝐽 ∧ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ∈ V ) → ( 𝑆 ‘ 𝑘 ) = { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
38 31 36 37 syl2anr ⊢ ( ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ 𝑘 ∈ 𝐽 ) → ( 𝑆 ‘ 𝑘 ) = { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
39 38 neeq1d ⊢ ( ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ 𝑘 ∈ 𝐽 ) → ( ( 𝑆 ‘ 𝑘 ) ≠ ∅ ↔ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ≠ ∅ ) )
40 rabn0 ⊢ ( { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ≠ ∅ ↔ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
41 39 40 bitrdi ⊢ ( ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ 𝑘 ∈ 𝐽 ) → ( ( 𝑆 ‘ 𝑘 ) ≠ ∅ ↔ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) )
42 41 anbi2d ⊢ ( ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ 𝑘 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ↔ ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
43 42 rexbidva ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ↔ ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
44 43 ralbidv ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
45 44 anbi2d ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) ↔ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) ) )
46 cnveq ⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
47 46 imaeq1d ⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ 𝑘 ) = ( ◡ 𝐹 “ 𝑘 ) )
48 47 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ↔ ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ) )
49 reseq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ↾ 𝑢 ) = ( 𝐹 ↾ 𝑢 ) )
50 49 eleq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ↔ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) )
51 50 anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
52 51 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
53 48 52 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ↔ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) )
54 53 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ↔ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) )
55 54 anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ↔ ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
56 55 rexbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ↔ ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
57 56 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
58 57 elrab ⊢ ( 𝐹 ∈ { 𝑓 ∈ ( 𝐶 Cn 𝐽 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) } ↔ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) ) )
59 45 58 bitr4di ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) ↔ 𝐹 ∈ { 𝑓 ∈ ( 𝐶 Cn 𝐽 ) ∣ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ∃ 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ( ∪ 𝑠 = ( ◡ 𝑓 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝑓 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) } ) )
60 30 59 bitr4d ⊢ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) ) )
61 7 60 biadanii ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ) ∧ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) ) )
62 3 5 61 3bitr4ri ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ↔ ( ( 𝐶 ∈ Top ∧ 𝐽 ∈ Top ∧ 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑘 ∈ 𝐽 ( 𝑥 ∈ 𝑘 ∧ ( 𝑆 ‘ 𝑘 ) ≠ ∅ ) ) )