Metamath Proof Explorer

Theorem cvmsi

Description: One direction of cvmsval . (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 cvmsi ⊢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 cvmsrcl ⊢T∈S⁡U→U∈J
3 imaeq2 ⊢k=U→F-1k=F-1U
4 3 eqeq2d ⊢k=U→⋃s=F-1k↔⋃s=F-1U
5 oveq2 ⊢k=U→J↾𝑡k=J↾𝑡U
6 5 oveq2d ⊢k=U→C↾𝑡uHomeoJ↾𝑡k=C↾𝑡uHomeoJ↾𝑡U
7 6 eleq2d ⊢k=U→F↾u∈C↾𝑡uHomeoJ↾𝑡k↔F↾u∈C↾𝑡uHomeoJ↾𝑡U
8 7 anbi2d ⊢k=U→∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
9 8 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
10 4 9 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
11 10 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
12 11 1 fvmptss2 ⊢S⁡U⊆s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
13 12 sseli ⊢T∈S⁡U→T∈s∈𝒫C∖∅|⋃s=F-1U∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
14 unieq ⊢s=T→⋃s=⋃T
15 14 eqeq1d ⊢s=T→⋃s=F-1U↔⋃T=F-1U
16 difeq1 ⊢s=T→s∖u=T∖u
17 16 raleqdv ⊢s=T→∀v∈s∖uu∩v=∅↔∀v∈T∖uu∩v=∅
18 17 anbi1d ⊢s=T→∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U↔∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
19 18 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
20 15 19 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
21 20 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
22 13 21 sylib ⊢T∈S⁡U→T∈𝒫C∖∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
23 22 simpld ⊢T∈S⁡U→T∈𝒫C∖∅
24 eldifsn ⊢T∈𝒫C∖∅↔T∈𝒫C∧T≠∅
25 23 24 sylib ⊢T∈S⁡U→T∈𝒫C∧T≠∅
26 elpwi ⊢T∈𝒫C→T⊆C
27 26 anim1i ⊢T∈𝒫C∧T≠∅→T⊆C∧T≠∅
28 25 27 syl ⊢T∈S⁡U→T⊆C∧T≠∅
29 22 simprd ⊢T∈S⁡U→⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U
30 2 28 29 3jca ⊢T∈S⁡U→U∈J∧T⊆C∧T≠∅∧⋃T=F-1U∧∀u∈T∀v∈T∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡U