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 -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
Assertion cvmscbv ⊢ S = a ∈ J ⟼ b ∈ 𝒫 C ∖ ∅ | ⋃ b = F -1 a ∧ ∀ c ∈ b ∀ d ∈ b ∖ c c ∩ d = ∅ ∧ F ↾ c ∈ C ↾ 𝑡 c Homeo J ↾ 𝑡 a

Proof

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