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 syl5bi ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉𝐽𝑉𝑈 ) ∧ 𝑥 ∈ ( 𝑆𝑈 ) ) ∧ 𝑡𝑥 ) → ( 𝑧 ∈ ran ( 𝑦𝑥 ↦ ( 𝑦 ∩ ( 𝐹𝑉 ) ) ) → ( 𝑧 ≠ ( 𝑡 ∩ ( 𝐹𝑉 ) ) → ( ( 𝑡 ∩ ( 𝐹𝑉 ) ) ∩ 𝑧 ) = ∅ ) ) )
94 93 impd ( ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉𝐽𝑉𝑈 ) ∧ 𝑥 ∈ ( 𝑆𝑈 ) ) ∧ 𝑡𝑥 ) → ( ( 𝑧 ∈ ran ( 𝑦𝑥 ↦ ( 𝑦 ∩ ( 𝐹𝑉 ) ) ) ∧ 𝑧 ≠ ( 𝑡 ∩ ( 𝐹𝑉 ) ) ) → ( ( 𝑡 ∩ ( 𝐹𝑉 ) ) ∩ 𝑧 ) = ∅ ) )
95 69 94 syl5bi ( ( ( ( 𝐹 ∈ ( 𝐶 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 syl5eq ( ( ( ( 𝐹 ∈ ( 𝐶 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 syl5bi ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑉𝐽𝑉𝑈 ) → ( ( 𝑆𝑈 ) ≠ ∅ → ( 𝑆𝑉 ) ≠ ∅ ) )