Metamath Proof Explorer

Theorem cvmsss2

Description: An open subset of an evenly covered set is evenly covered. (Contributed by Mario Carneiro, 7-Jul-2015)

Ref Expression
Hypothesis cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmsss2 ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑆 ‘ 𝑈 ) ≠ ∅ → ( 𝑆 ‘ 𝑉 ) ≠ ∅ ) )

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 n0 ⊢ ( ( 𝑆 ‘ 𝑈 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) )
3 simpl2 ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝑉 ∈ 𝐽 )
4 simpl1 ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
6 4 5 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝐶 ∈ Top )
7 6 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝐶 ∈ Top )
8 1 cvmsss ⊢ ( 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑥 ⊆ 𝐶 )
9 8 adantl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝑥 ⊆ 𝐶 )
10 9 sselda ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐶 )
11 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
12 4 11 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
13 cnima ⊢ ( ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ∧ 𝑉 ∈ 𝐽 ) → ( ◡ 𝐹 “ 𝑉 ) ∈ 𝐶 )
14 12 3 13 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( ◡ 𝐹 “ 𝑉 ) ∈ 𝐶 )
15 14 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ◡ 𝐹 “ 𝑉 ) ∈ 𝐶 )
16 inopn ⊢ ( ( 𝐶 ∈ Top ∧ 𝑦 ∈ 𝐶 ∧ ( ◡ 𝐹 “ 𝑉 ) ∈ 𝐶 ) → ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ 𝐶 )
17 7 10 15 16 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ 𝐶 )
18 17 fmpttd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) : 𝑥 ⟶ 𝐶 )
19 18 frnd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ 𝐶 )
20 1 cvmsn0 ⊢ ( 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑥 ≠ ∅ )
21 20 adantl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝑥 ≠ ∅ )
22 dmmptg ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ V → dom ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = 𝑥 )
23 inex1g ⊢ ( 𝑦 ∈ 𝑥 → ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ V )
24 22 23 mprg ⊢ dom ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = 𝑥
25 24 eqeq1i ⊢ ( dom ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ∅ ↔ 𝑥 = ∅ )
26 dm0rn0 ⊢ ( dom ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ∅ ↔ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ∅ )
27 25 26 bitr3i ⊢ ( 𝑥 = ∅ ↔ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ∅ )
28 27 necon3bii ⊢ ( 𝑥 ≠ ∅ ↔ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ≠ ∅ )
29 21 28 sylib ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ≠ ∅ )
30 19 29 jca ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ 𝐶 ∧ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ≠ ∅ ) )
31 inss2 ⊢ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑉 )
32 elpw2g ⊢ ( ( ◡ 𝐹 “ 𝑉 ) ∈ 𝐶 → ( ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ 𝒫 ( ◡ 𝐹 “ 𝑉 ) ↔ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑉 ) ) )
33 15 32 syl ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ 𝒫 ( ◡ 𝐹 “ 𝑉 ) ↔ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ ( ◡ 𝐹 “ 𝑉 ) ) )
34 31 33 mpbiri ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ 𝒫 ( ◡ 𝐹 “ 𝑉 ) )
35 34 fmpttd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) : 𝑥 ⟶ 𝒫 ( ◡ 𝐹 “ 𝑉 ) )
36 35 frnd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ 𝒫 ( ◡ 𝐹 “ 𝑉 ) )
37 sspwuni ⊢ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ 𝒫 ( ◡ 𝐹 “ 𝑉 ) ↔ ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ ( ◡ 𝐹 “ 𝑉 ) )
38 36 37 sylib ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ ( ◡ 𝐹 “ 𝑉 ) )
39 simpl3 ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝑉 ⊆ 𝑈 )
40 imass2 ⊢ ( 𝑉 ⊆ 𝑈 → ( ◡ 𝐹 “ 𝑉 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) )
41 39 40 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( ◡ 𝐹 “ 𝑉 ) ⊆ ( ◡ 𝐹 “ 𝑈 ) )
42 1 cvmsuni ⊢ ( 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) → ∪ 𝑥 = ( ◡ 𝐹 “ 𝑈 ) )
43 42 adantl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ∪ 𝑥 = ( ◡ 𝐹 “ 𝑈 ) )
44 41 43 sseqtrrd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( ◡ 𝐹 “ 𝑉 ) ⊆ ∪ 𝑥 )
45 44 sselda ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) → 𝑧 ∈ ∪ 𝑥 )
46 eqid ⊢ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) )
47 ineq1 ⊢ ( 𝑦 = 𝑡 → ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
48 47 rspceeqv ⊢ ( ( 𝑡 ∈ 𝑥 ∧ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
49 46 48 mpan2 ⊢ ( 𝑡 ∈ 𝑥 → ∃ 𝑦 ∈ 𝑥 ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
50 49 ad2antrl ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) ∧ ( 𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡 ) ) → ∃ 𝑦 ∈ 𝑥 ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
51 vex ⊢ 𝑡 ∈ V
52 51 inex1 ⊢ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ V
53 eqid ⊢ ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
54 53 elrnmpt ⊢ ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ V → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
55 52 54 ax-mp ⊢ ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑥 ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
56 50 55 sylibr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) ∧ ( 𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡 ) ) → ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
57 simprr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) ∧ ( 𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡 ) ) → 𝑧 ∈ 𝑡 )
58 simplr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) ∧ ( 𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) )
59 57 58 elind ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) ∧ ( 𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡 ) ) → 𝑧 ∈ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
60 eleq2 ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
61 60 rspcev ⊢ ( ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∧ 𝑧 ∈ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) → ∃ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) 𝑧 ∈ 𝑤 )
62 56 59 61 syl2anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) ∧ ( 𝑡 ∈ 𝑥 ∧ 𝑧 ∈ 𝑡 ) ) → ∃ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) 𝑧 ∈ 𝑤 )
63 62 rexlimdvaa ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) → ( ∃ 𝑡 ∈ 𝑥 𝑧 ∈ 𝑡 → ∃ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) 𝑧 ∈ 𝑤 ) )
64 eluni2 ⊢ ( 𝑧 ∈ ∪ 𝑥 ↔ ∃ 𝑡 ∈ 𝑥 𝑧 ∈ 𝑡 )
65 eluni2 ⊢ ( 𝑧 ∈ ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ↔ ∃ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) 𝑧 ∈ 𝑤 )
66 63 64 65 3imtr4g ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝑧 ∈ ∪ 𝑥 → 𝑧 ∈ ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ) )
67 45 66 mpd ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑧 ∈ ( ◡ 𝐹 “ 𝑉 ) ) → 𝑧 ∈ ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
68 38 67 eqelssd ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( ◡ 𝐹 “ 𝑉 ) )
69 eldifsn ⊢ ( 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ↔ ( 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∧ 𝑧 ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
70 vex ⊢ 𝑧 ∈ V
71 53 elrnmpt ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑥 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
72 70 71 ax-mp ⊢ ( 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ↔ ∃ 𝑦 ∈ 𝑥 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
73 47 equcoms ⊢ ( 𝑡 = 𝑦 → ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
74 73 necon3ai ⊢ ( ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ¬ 𝑡 = 𝑦 )
75 simpllr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) )
76 simplr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑡 ∈ 𝑥 )
77 simpr ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 )
78 1 cvmsdisj ⊢ ( ( 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝑡 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥 ) → ( 𝑡 = 𝑦 ∨ ( 𝑡 ∩ 𝑦 ) = ∅ ) )
79 75 76 77 78 syl3anc ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑡 = 𝑦 ∨ ( 𝑡 ∩ 𝑦 ) = ∅ ) )
80 79 ord ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( ¬ 𝑡 = 𝑦 → ( 𝑡 ∩ 𝑦 ) = ∅ ) )
81 inss1 ⊢ ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ ( 𝑡 ∩ 𝑦 )
82 sseq0 ⊢ ( ( ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ ( 𝑡 ∩ 𝑦 ) ∧ ( 𝑡 ∩ 𝑦 ) = ∅ ) → ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ∅ )
83 81 82 mpan ⊢ ( ( 𝑡 ∩ 𝑦 ) = ∅ → ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ∅ )
84 74 80 83 syl56 ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ∅ ) )
85 neeq1 ⊢ ( 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝑧 ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ↔ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
86 ineq2 ⊢ ( 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
87 inindir ⊢ ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
88 86 87 eqtr4di ⊢ ( 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
89 88 eqeq1d ⊢ ( 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ↔ ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ∅ ) )
90 85 89 imbi12d ⊢ ( 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑧 ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) ↔ ( ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ∅ ) ) )
91 84 90 syl5ibrcom ⊢ ( ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝑧 ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) ) )
92 91 rexlimdva ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ∃ 𝑦 ∈ 𝑥 𝑧 = ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝑧 ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) ) )
93 72 92 biimtrid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) → ( 𝑧 ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) ) )
94 93 impd ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝑧 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∧ 𝑧 ≠ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) )
95 69 94 biimtrid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) → ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) )
96 95 ralrimiv ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ )
97 inss1 ⊢ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ 𝑡
98 resabs1 ⊢ ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ 𝑡 → ( ( 𝐹 ↾ 𝑡 ) ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
99 97 98 ax-mp ⊢ ( ( 𝐹 ↾ 𝑡 ) ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
100 1 cvmshmeo ⊢ ( ( 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝐹 ↾ 𝑡 ) ∈ ( ( 𝐶 ↾t 𝑡 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
101 100 adantll ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝐹 ↾ 𝑡 ) ∈ ( ( 𝐶 ↾t 𝑡 ) Homeo ( 𝐽 ↾t 𝑈 ) ) )
102 6 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝐶 ∈ Top )
103 9 sselda ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝑡 ∈ 𝐶 )
104 elssuni ⊢ ( 𝑡 ∈ 𝐶 → 𝑡 ⊆ ∪ 𝐶 )
105 103 104 syl ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝑡 ⊆ ∪ 𝐶 )
106 eqid ⊢ ∪ 𝐶 = ∪ 𝐶
107 106 restuni ⊢ ( ( 𝐶 ∈ Top ∧ 𝑡 ⊆ ∪ 𝐶 ) → 𝑡 = ∪ ( 𝐶 ↾t 𝑡 ) )
108 102 105 107 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝑡 = ∪ ( 𝐶 ↾t 𝑡 ) )
109 97 108 sseqtrid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ ∪ ( 𝐶 ↾t 𝑡 ) )
110 eqid ⊢ ∪ ( 𝐶 ↾t 𝑡 ) = ∪ ( 𝐶 ↾t 𝑡 )
111 110 hmeores ⊢ ( ( ( 𝐹 ↾ 𝑡 ) ∈ ( ( 𝐶 ↾t 𝑡 ) Homeo ( 𝐽 ↾t 𝑈 ) ) ∧ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ ∪ ( 𝐶 ↾t 𝑡 ) ) → ( ( 𝐹 ↾ 𝑡 ) ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( ( 𝐶 ↾t 𝑡 ) ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( ( 𝐽 ↾t 𝑈 ) ↾t ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ) ) )
112 101 109 111 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑡 ) ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( ( 𝐶 ↾t 𝑡 ) ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( ( 𝐽 ↾t 𝑈 ) ↾t ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ) ) )
113 99 112 eqeltrrid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( ( 𝐶 ↾t 𝑡 ) ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( ( 𝐽 ↾t 𝑈 ) ↾t ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ) ) )
114 97 a1i ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ 𝑡 )
115 simpr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝑡 ∈ 𝑥 )
116 restabs ⊢ ( ( 𝐶 ∈ Top ∧ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ⊆ 𝑡 ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐶 ↾t 𝑡 ) ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
117 102 114 115 116 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐶 ↾t 𝑡 ) ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
118 incom ⊢ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( ( ◡ 𝐹 “ 𝑉 ) ∩ 𝑡 )
119 cnvresima ⊢ ( ◡ ( 𝐹 ↾ 𝑡 ) “ 𝑉 ) = ( ( ◡ 𝐹 “ 𝑉 ) ∩ 𝑡 )
120 118 119 eqtr4i ⊢ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) = ( ◡ ( 𝐹 ↾ 𝑡 ) “ 𝑉 )
121 120 imaeq2i ⊢ ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( ( 𝐹 ↾ 𝑡 ) “ ( ◡ ( 𝐹 ↾ 𝑡 ) “ 𝑉 ) )
122 4 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
123 simplr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) )
124 1 cvmsf1o ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝐹 ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑈 )
125 122 123 115 124 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝐹 ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑈 )
126 f1ofo ⊢ ( ( 𝐹 ↾ 𝑡 ) : 𝑡 –1-1-onto→ 𝑈 → ( 𝐹 ↾ 𝑡 ) : 𝑡 –onto→ 𝑈 )
127 125 126 syl ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝐹 ↾ 𝑡 ) : 𝑡 –onto→ 𝑈 )
128 39 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → 𝑉 ⊆ 𝑈 )
129 foimacnv ⊢ ( ( ( 𝐹 ↾ 𝑡 ) : 𝑡 –onto→ 𝑈 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝐹 ↾ 𝑡 ) “ ( ◡ ( 𝐹 ↾ 𝑡 ) “ 𝑉 ) ) = 𝑉 )
130 127 128 129 syl2anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑡 ) “ ( ◡ ( 𝐹 ↾ 𝑡 ) “ 𝑉 ) ) = 𝑉 )
131 121 130 eqtrid ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = 𝑉 )
132 131 oveq2d ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐽 ↾t 𝑈 ) ↾t ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ) = ( ( 𝐽 ↾t 𝑈 ) ↾t 𝑉 ) )
133 cvmtop2 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )
134 4 133 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝐽 ∈ Top )
135 1 cvmsrcl ⊢ ( 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) → 𝑈 ∈ 𝐽 )
136 135 adantl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → 𝑈 ∈ 𝐽 )
137 restabs ⊢ ( ( 𝐽 ∈ Top ∧ 𝑉 ⊆ 𝑈 ∧ 𝑈 ∈ 𝐽 ) → ( ( 𝐽 ↾t 𝑈 ) ↾t 𝑉 ) = ( 𝐽 ↾t 𝑉 ) )
138 134 39 136 137 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( ( 𝐽 ↾t 𝑈 ) ↾t 𝑉 ) = ( 𝐽 ↾t 𝑉 ) )
139 138 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐽 ↾t 𝑈 ) ↾t 𝑉 ) = ( 𝐽 ↾t 𝑉 ) )
140 132 139 eqtrd ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( 𝐽 ↾t 𝑈 ) ↾t ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ) = ( 𝐽 ↾t 𝑉 ) )
141 117 140 oveq12d ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ( ( 𝐶 ↾t 𝑡 ) ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( ( 𝐽 ↾t 𝑈 ) ↾t ( ( 𝐹 ↾ 𝑡 ) “ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ) ) = ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) )
142 113 141 eleqtrd ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) )
143 96 142 jca ⊢ ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) ∧ 𝑡 ∈ 𝑥 ) → ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) )
144 143 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ∀ 𝑡 ∈ 𝑥 ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) )
145 52 rgenw ⊢ ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ V
146 47 cbvmptv ⊢ ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( 𝑡 ∈ 𝑥 ↦ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) )
147 sneq ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → { 𝑤 } = { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } )
148 147 difeq2d ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) = ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) )
149 ineq1 ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝑤 ∩ 𝑧 ) = ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) )
150 149 eqeq1d ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝑤 ∩ 𝑧 ) = ∅ ↔ ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) )
151 148 150 raleqbidv ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ↔ ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ) )
152 reseq2 ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝐹 ↾ 𝑤 ) = ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
153 oveq2 ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( 𝐶 ↾t 𝑤 ) = ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) )
154 153 oveq1d ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) = ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) )
155 152 154 eleq12d ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ↔ ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) )
156 151 155 anbi12d ⊢ ( 𝑤 = ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) → ( ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ↔ ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ) )
157 146 156 ralrnmptw ⊢ ( ∀ 𝑡 ∈ 𝑥 ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∈ V → ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ) )
158 145 157 ax-mp ⊢ ( ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ↔ ∀ 𝑡 ∈ 𝑥 ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) } ) ( ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( ( 𝐶 ↾t ( 𝑡 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) )
159 144 158 sylibr ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) )
160 68 159 jca ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( ◡ 𝐹 “ 𝑉 ) ∧ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ) )
161 1 cvmscbv ⊢ 𝑆 = ( 𝑎 ∈ 𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑤 ∈ 𝑏 ( ∀ 𝑧 ∈ ( 𝑏 ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )
162 161 cvmsval ⊢ ( 𝐶 ∈ Top → ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( 𝑆 ‘ 𝑉 ) ↔ ( 𝑉 ∈ 𝐽 ∧ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ 𝐶 ∧ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ≠ ∅ ) ∧ ( ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( ◡ 𝐹 “ 𝑉 ) ∧ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ) ) ) )
163 6 162 syl ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( 𝑆 ‘ 𝑉 ) ↔ ( 𝑉 ∈ 𝐽 ∧ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ⊆ 𝐶 ∧ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ≠ ∅ ) ∧ ( ∪ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) = ( ◡ 𝐹 “ 𝑉 ) ∧ ∀ 𝑤 ∈ ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ( ∀ 𝑧 ∈ ( ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∖ { 𝑤 } ) ( 𝑤 ∩ 𝑧 ) = ∅ ∧ ( 𝐹 ↾ 𝑤 ) ∈ ( ( 𝐶 ↾t 𝑤 ) Homeo ( 𝐽 ↾t 𝑉 ) ) ) ) ) ) )
164 3 30 160 163 mpbir3and ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ran ( 𝑦 ∈ 𝑥 ↦ ( 𝑦 ∩ ( ◡ 𝐹 “ 𝑉 ) ) ) ∈ ( 𝑆 ‘ 𝑉 ) )
165 164 ne0d ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) ) → ( 𝑆 ‘ 𝑉 ) ≠ ∅ )
166 165 ex ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑆 ‘ 𝑉 ) ≠ ∅ ) )
167 166 exlimdv ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) → ( ∃ 𝑥 𝑥 ∈ ( 𝑆 ‘ 𝑈 ) → ( 𝑆 ‘ 𝑉 ) ≠ ∅ ) )
168 2 167 biimtrid ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉 ∈ 𝐽 ∧ 𝑉 ⊆ 𝑈 ) → ( ( 𝑆 ‘ 𝑈 ) ≠ ∅ → ( 𝑆 ‘ 𝑉 ) ≠ ∅ ) )