Metamath Proof Explorer

Theorem cvmscbv

Description: Change bound variables in the set of even coverings. (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Hypothesis iscvm.1 ⊢S=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
Assertion cvmscbv ⊢S=a∈J⟼b∈𝒫C∖∅|⋃b=F-1a∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a

Proof

Step Hyp Ref Expression
1 iscvm.1 ⊢S=k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k
2 unieq ⊢s=b→⋃s=⋃b
3 2 eqeq1d ⊢s=b→⋃s=F-1k↔⋃b=F-1k
4 ineq2 ⊢v=d→u∩v=u∩d
5 4 eqeq1d ⊢v=d→u∩v=∅↔u∩d=∅
6 5 cbvralvw ⊢∀v∈s∖uu∩v=∅↔∀d∈s∖uu∩d=∅
7 sneq ⊢u=c→u=c
8 7 difeq2d ⊢u=c→s∖u=s∖c
9 ineq1 ⊢u=c→u∩d=c∩d
10 9 eqeq1d ⊢u=c→u∩d=∅↔c∩d=∅
11 8 10 raleqbidv ⊢u=c→∀d∈s∖uu∩d=∅↔∀d∈s∖cc∩d=∅
12 6 11 bitrid ⊢u=c→∀v∈s∖uu∩v=∅↔∀d∈s∖cc∩d=∅
13 reseq2 ⊢u=c→F↾u=F↾c
14 oveq2 ⊢u=c→C↾𝑡u=C↾𝑡c
15 14 oveq1d ⊢u=c→C↾𝑡uHomeoJ↾𝑡k=C↾𝑡cHomeoJ↾𝑡k
16 13 15 eleq12d ⊢u=c→F↾u∈C↾𝑡uHomeoJ↾𝑡k↔F↾c∈C↾𝑡cHomeoJ↾𝑡k
17 12 16 anbi12d ⊢u=c→∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔∀d∈s∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k
18 17 cbvralvw ⊢∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔∀c∈s∀d∈s∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k
19 difeq1 ⊢s=b→s∖c=b∖c
20 19 raleqdv ⊢s=b→∀d∈s∖cc∩d=∅↔∀d∈b∖cc∩d=∅
21 20 anbi1d ⊢s=b→∀d∈s∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k↔∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k
22 21 raleqbi1dv ⊢s=b→∀c∈s∀d∈s∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k↔∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k
23 18 22 bitrid ⊢s=b→∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k
24 3 23 anbi12d ⊢s=b→⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k↔⋃b=F-1k∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k
25 24 cbvrabv ⊢s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k=b∈𝒫C∖∅|⋃b=F-1k∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k
26 imaeq2 ⊢k=a→F-1k=F-1a
27 26 eqeq2d ⊢k=a→⋃b=F-1k↔⋃b=F-1a
28 oveq2 ⊢k=a→J↾𝑡k=J↾𝑡a
29 28 oveq2d ⊢k=a→C↾𝑡cHomeoJ↾𝑡k=C↾𝑡cHomeoJ↾𝑡a
30 29 eleq2d ⊢k=a→F↾c∈C↾𝑡cHomeoJ↾𝑡k↔F↾c∈C↾𝑡cHomeoJ↾𝑡a
31 30 anbi2d ⊢k=a→∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k↔∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a
32 31 ralbidv ⊢k=a→∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k↔∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a
33 27 32 anbi12d ⊢k=a→⋃b=F-1k∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k↔⋃b=F-1a∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a
34 33 rabbidv ⊢k=a→b∈𝒫C∖∅|⋃b=F-1k∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡k=b∈𝒫C∖∅|⋃b=F-1a∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a
35 25 34 eqtrid ⊢k=a→s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k=b∈𝒫C∖∅|⋃b=F-1a∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a
36 35 cbvmptv ⊢k∈J⟼s∈𝒫C∖∅|⋃s=F-1k∧∀u∈s∀v∈s∖uu∩v=∅∧F↾u∈C↾𝑡uHomeoJ↾𝑡k=a∈J⟼b∈𝒫C∖∅|⋃b=F-1a∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a
37 1 36 eqtri ⊢S=a∈J⟼b∈𝒫C∖∅|⋃b=F-1a∧∀c∈b∀d∈b∖cc∩d=∅∧F↾c∈C↾𝑡cHomeoJ↾𝑡a