Metamath Proof Explorer

Theorem cvmsval

Description: Elementhood in the set S of all even coverings of an open set in J . S is an even covering of U if it is a nonempty collection of disjoint open sets in C whose union is the preimage of U , such that each set u e. S is homeomorphic under F to U . (Contributed by Mario Carneiro, 13-Feb-2015)

Ref Expression
Hypothesis cvmcov.1 ⊢S=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
Assertion cvmsval ⊢C∈V→T∈S⁡U↔U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U

Proof

Step Hyp Ref Expression
1 cvmcov.1 ⊢S=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
2 1 cvmsi ⊢T∈S⁡U→U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
3 3anass ⊢U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
4 id ⊢U∈J→U∈J
5 pwexg ⊢C∈V→𝒫C∈V
6 difexg ⊢𝒫C∈V→𝒫C∖∅∈V
7 rabexg ⊢𝒫C∖∅∈V→s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U∈V
8 5 6 7 3syl ⊢C∈V→s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U∈V
9 imaeq2 ⊢k=U→F-1k=F-1U
10 9 eqeq2d ⊢k=U→⋃s=F-1k↔⋃s=F-1U
11 oveq2 ⊢k=U→J↾𝑡k=J↾𝑡U
12 11 oveq2d ⊢k=U→C↾𝑡uHomeoJ↾𝑡k=C↾𝑡uHomeoJ↾𝑡U
13 12 eleq2d ⊢k=U→F↾u∈C↾𝑡uHomeoJ↾𝑡k↔F↾u∈C↾𝑡uHomeoJ↾𝑡U
14 13 anbi2d ⊢k=U→∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
15 14 ralbidv ⊢k=U→∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
16 10 15 anbi12d ⊢k=U→⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
17 16 rabbidv ⊢k=U→s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k=s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
18 17 1 fvmptg ⊢U∈J∧s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U∈V→S⁡U=s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
19 4 8 18 syl2anr ⊢C∈V∧U∈J→S⁡U=s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
20 19 eleq2d ⊢C∈V∧U∈J→T∈S⁡U↔T∈s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
21 unieq ⊢s=T→⋃s=⋃T
22 21 eqeq1d ⊢s=T→⋃s=F-1U↔⋃T=F-1U
23 difeq1 ⊢s=T→s∖u=T∖u
24 23 raleqdv ⊢s=T→∀v∈s∖uu∩v=∅↔∀v∈T∖uu∩v=∅
25 24 anbi1d ⊢s=T→∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
26 25 raleqbi1dv ⊢s=T→∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
27 22 26 anbi12d ⊢s=T→⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
28 27 elrab ⊢T∈s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔T∈𝒫C∖∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
29 eldifsn ⊢T∈𝒫C∖∅↔T∈𝒫C∧T≠∅
30 elpw2g ⊢C∈V→T∈𝒫C↔T⊆C
31 30 adantr ⊢C∈V∧U∈J→T∈𝒫C↔T⊆C
32 31 anbi1d ⊢C∈V∧U∈J→T∈𝒫C∧T≠∅↔T⊆C∧T≠∅
33 29 32 bitrid ⊢C∈V∧U∈J→T∈𝒫C∖∅↔T⊆C∧T≠∅
34 33 anbi1d ⊢C∈V∧U∈J→T∈𝒫C∖∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
35 28 34 bitrid ⊢C∈V∧U∈J→T∈s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
36 20 35 bitrd ⊢C∈V∧U∈J→T∈S⁡U↔T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
37 36 biimprd ⊢C∈V∧U∈J→T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U→T∈S⁡U
38 37 expimpd ⊢C∈V→U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U→T∈S⁡U
39 3 38 biimtrid ⊢C∈V→U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U→T∈S⁡U
40 2 39 impbid2 ⊢C∈V→T∈S⁡U↔U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U