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 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmscbv 𝑆 = ( 𝑎 ∈ 𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 iscvm.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 unieq ⊢ ( 𝑠 = 𝑏 → ∪ 𝑠 = ∪ 𝑏 )
3 2 eqeq1d ⊢ ( 𝑠 = 𝑏 → ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ↔ ∪ 𝑏 = ( ◡ 𝐹 “ 𝑘 ) ) )
4 ineq2 ⊢ ( 𝑣 = 𝑑 → ( 𝑢 ∩ 𝑣 ) = ( 𝑢 ∩ 𝑑 ) )
5 4 eqeq1d ⊢ ( 𝑣 = 𝑑 → ( ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ( 𝑢 ∩ 𝑑 ) = ∅ ) )
6 5 cbvralvw ⊢ ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑑 ) = ∅ )
7 sneq ⊢ ( 𝑢 = 𝑐 → { 𝑢 } = { 𝑐 } )
8 7 difeq2d ⊢ ( 𝑢 = 𝑐 → ( 𝑠 ∖ { 𝑢 } ) = ( 𝑠 ∖ { 𝑐 } ) )
9 ineq1 ⊢ ( 𝑢 = 𝑐 → ( 𝑢 ∩ 𝑑 ) = ( 𝑐 ∩ 𝑑 ) )
10 9 eqeq1d ⊢ ( 𝑢 = 𝑐 → ( ( 𝑢 ∩ 𝑑 ) = ∅ ↔ ( 𝑐 ∩ 𝑑 ) = ∅ ) )
11 8 10 raleqbidv ⊢ ( 𝑢 = 𝑐 → ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑑 ) = ∅ ↔ ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ) )
12 6 11 syl5bb ⊢ ( 𝑢 = 𝑐 → ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ↔ ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ) )
13 reseq2 ⊢ ( 𝑢 = 𝑐 → ( 𝐹 ↾ 𝑢 ) = ( 𝐹 ↾ 𝑐 ) )
14 oveq2 ⊢ ( 𝑢 = 𝑐 → ( 𝐶 ↾t 𝑢 ) = ( 𝐶 ↾t 𝑐 ) )
15 14 oveq1d ⊢ ( 𝑢 = 𝑐 → ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) = ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) )
16 13 15 eleq12d ⊢ ( 𝑢 = 𝑐 → ( ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ↔ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) )
17 12 16 anbi12d ⊢ ( 𝑢 = 𝑐 → ( ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
18 17 cbvralvw ⊢ ( ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) )
19 difeq1 ⊢ ( 𝑠 = 𝑏 → ( 𝑠 ∖ { 𝑐 } ) = ( 𝑏 ∖ { 𝑐 } ) )
20 19 raleqdv ⊢ ( 𝑠 = 𝑏 → ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ↔ ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ) )
21 20 anbi1d ⊢ ( 𝑠 = 𝑏 → ( ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
22 21 raleqbi1dv ⊢ ( 𝑠 = 𝑏 → ( ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
23 18 22 syl5bb ⊢ ( 𝑠 = 𝑏 → ( ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) )
24 3 23 anbi12d ⊢ ( 𝑠 = 𝑏 → ( ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ↔ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ) )
25 24 cbvrabv ⊢ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } = { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) }
26 imaeq2 ⊢ ( 𝑘 = 𝑎 → ( ◡ 𝐹 “ 𝑘 ) = ( ◡ 𝐹 “ 𝑎 ) )
27 26 eqeq2d ⊢ ( 𝑘 = 𝑎 → ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑘 ) ↔ ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ) )
28 oveq2 ⊢ ( 𝑘 = 𝑎 → ( 𝐽 ↾t 𝑘 ) = ( 𝐽 ↾t 𝑎 ) )
29 28 oveq2d ⊢ ( 𝑘 = 𝑎 → ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) = ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) )
30 29 eleq2d ⊢ ( 𝑘 = 𝑎 → ( ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ↔ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) )
31 30 anbi2d ⊢ ( 𝑘 = 𝑎 → ( ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) )
32 31 ralbidv ⊢ ( 𝑘 = 𝑎 → ( ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ↔ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) )
33 27 32 anbi12d ⊢ ( 𝑘 = 𝑎 → ( ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) ↔ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) ) )
34 33 rabbidv ⊢ ( 𝑘 = 𝑎 → { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } = { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )
35 25 34 eqtrid ⊢ ( 𝑘 = 𝑎 → { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } = { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )
36 35 cbvmptv ⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑎 ∈ 𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )
37 1 36 eqtri ⊢ 𝑆 = ( 𝑎 ∈ 𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )