Metamath Proof Explorer

Theorem cvmopnlem

Description: Lemma for cvmopn . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmseu.1 ⊢ 𝐵 = ∪ 𝐶
Assertion cvmopnlem ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → ( 𝐹 “ 𝐴 ) ∈ 𝐽 )

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmseu.1 ⊢ 𝐵 = ∪ 𝐶
3 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
5 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 2 6 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
8 5 7 syl ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
9 8 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
10 elssuni ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ⊆ ∪ 𝐶 )
11 10 2 sseqtrrdi ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ⊆ 𝐵 )
12 11 adantl ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → 𝐴 ⊆ 𝐵 )
13 12 sselda ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
14 9 13 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ∪ 𝐽 )
15 1 6 cvmcov ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ∪ 𝐽 ) → ∃ 𝑡 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ ( 𝑆 ‘ 𝑡 ) ≠ ∅ ) )
16 3 14 15 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑡 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ ( 𝑆 ‘ 𝑡 ) ≠ ∅ ) )
17 n0 ⊢ ( ( 𝑆 ‘ 𝑡 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) )
18 inss2 ⊢ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ⊆ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 )
19 resima2 ⊢ ( ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ⊆ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) → ( ( 𝐹 ↾ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) = ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) )
20 18 19 ax-mp ⊢ ( ( 𝐹 ↾ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) = ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) )
21 simprr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) )
22 3 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
23 13 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝑧 ∈ 𝐵 )
24 simprl ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 )
25 eqid ⊢ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) = ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 )
26 1 2 25 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ∧ 𝑧 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) ) → ( ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ∈ 𝑤 ∧ 𝑧 ∈ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) )
27 22 21 23 24 26 syl13anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ∈ 𝑤 ∧ 𝑧 ∈ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) )
28 27 simpld ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ∈ 𝑤 )
29 1 cvmshmeo ⊢ ( ( 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ∧ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ∈ 𝑤 ) → ( 𝐹 ↾ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ∈ ( ( 𝐶 ↾t ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) Homeo ( 𝐽 ↾t 𝑡 ) ) )
30 21 28 29 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐹 ↾ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ∈ ( ( 𝐶 ↾t ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) Homeo ( 𝐽 ↾t 𝑡 ) ) )
31 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
32 22 31 syl ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝐶 ∈ Top )
33 simpllr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝐴 ∈ 𝐶 )
34 elrestr ⊢ ( ( 𝐶 ∈ Top ∧ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ∈ 𝑤 ∧ 𝐴 ∈ 𝐶 ) → ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ∈ ( 𝐶 ↾t ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) )
35 32 28 33 34 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ∈ ( 𝐶 ↾t ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) )
36 hmeoima ⊢ ( ( ( 𝐹 ↾ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ∈ ( ( 𝐶 ↾t ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) Homeo ( 𝐽 ↾t 𝑡 ) ) ∧ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ∈ ( 𝐶 ↾t ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) → ( ( 𝐹 ↾ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ ( 𝐽 ↾t 𝑡 ) )
37 30 35 36 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( ( 𝐹 ↾ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ ( 𝐽 ↾t 𝑡 ) )
38 20 37 eqeltrrid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ ( 𝐽 ↾t 𝑡 ) )
39 cvmtop2 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )
40 39 adantr ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → 𝐽 ∈ Top )
41 40 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝐽 ∈ Top )
42 1 cvmsrcl ⊢ ( 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) → 𝑡 ∈ 𝐽 )
43 42 ad2antll ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝑡 ∈ 𝐽 )
44 restopn2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑡 ∈ 𝐽 ) → ( ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ ( 𝐽 ↾t 𝑡 ) ↔ ( ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ 𝐽 ∧ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ 𝑡 ) ) )
45 41 43 44 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ ( 𝐽 ↾t 𝑡 ) ↔ ( ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ 𝐽 ∧ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ 𝑡 ) ) )
46 38 45 mpbid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ 𝐽 ∧ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ 𝑡 ) )
47 46 simpld ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ 𝐽 )
48 8 ffnd ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → 𝐹 Fn 𝐵 )
49 48 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝐹 Fn 𝐵 )
50 inss1 ⊢ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ⊆ 𝐴
51 33 11 syl ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝐴 ⊆ 𝐵 )
52 50 51 sstrid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ⊆ 𝐵 )
53 simplr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝑧 ∈ 𝐴 )
54 27 simprd ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝑧 ∈ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) )
55 53 54 elind ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → 𝑧 ∈ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) )
56 fnfvima ⊢ ( ( 𝐹 Fn 𝐵 ∧ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ⊆ 𝐵 ∧ 𝑧 ∈ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) )
57 49 52 55 56 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) )
58 imass2 ⊢ ( ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ⊆ 𝐴 → ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ ( 𝐹 “ 𝐴 ) )
59 50 58 mp1i ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ ( 𝐹 “ 𝐴 ) )
60 eleq2 ⊢ ( 𝑦 = ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ) )
61 sseq1 ⊢ ( 𝑦 = ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) → ( 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ ( 𝐹 “ 𝐴 ) ) )
62 60 61 anbi12d ⊢ ( 𝑦 = ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∧ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ ( 𝐹 “ 𝐴 ) ) ) )
63 62 rspcev ⊢ ( ( ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∈ 𝐽 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ∧ ( 𝐹 “ ( 𝐴 ∩ ( ℩ 𝑥 ∈ 𝑤 𝑧 ∈ 𝑥 ) ) ) ⊆ ( 𝐹 “ 𝐴 ) ) ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) )
64 47 57 59 63 syl12anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) ) ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) )
65 64 expr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) → ( 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
66 65 exlimdv ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) → ( ∃ 𝑤 𝑤 ∈ ( 𝑆 ‘ 𝑡 ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
67 17 66 syl5bi ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) → ( ( 𝑆 ‘ 𝑡 ) ≠ ∅ → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
68 67 expimpd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ ( 𝑆 ‘ 𝑡 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
69 68 rexlimdvw ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑡 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ∧ ( 𝑆 ‘ 𝑡 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
70 16 69 mpd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) )
71 70 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) )
72 eleq1 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ) )
73 72 anbi1d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
74 73 rexbidv ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑧 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ↔ ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
75 74 ralima ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐴 ) ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
76 48 12 75 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐴 ) ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑦 ∈ 𝐽 ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
77 71 76 mpbird ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝐴 ) ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) )
78 eltop2 ⊢ ( 𝐽 ∈ Top → ( ( 𝐹 “ 𝐴 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( 𝐹 “ 𝐴 ) ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
79 40 78 syl ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → ( ( 𝐹 “ 𝐴 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( 𝐹 “ 𝐴 ) ∃ 𝑦 ∈ 𝐽 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ ( 𝐹 “ 𝐴 ) ) ) )
80 77 79 mpbird ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐴 ∈ 𝐶 ) → ( 𝐹 “ 𝐴 ) ∈ 𝐽 )