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 syl5eq ( 𝑘 = 𝑎 → { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } = { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑏 = ( 𝐹𝑎 ) ∧ ∀ 𝑐𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐𝑑 ) = ∅ ∧ ( 𝐹𝑐 ) ∈ ( ( 𝐶t 𝑐 ) Homeo ( 𝐽t 𝑎 ) ) ) ) } )
36 35 cbvmptv ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } ) = ( 𝑎𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑏 = ( 𝐹𝑎 ) ∧ ∀ 𝑐𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐𝑑 ) = ∅ ∧ ( 𝐹𝑐 ) ∈ ( ( 𝐶t 𝑐 ) Homeo ( 𝐽t 𝑎 ) ) ) ) } )
37 1 36 eqtri 𝑆 = ( 𝑎𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑏 = ( 𝐹𝑎 ) ∧ ∀ 𝑐𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐𝑑 ) = ∅ ∧ ( 𝐹𝑐 ) ∈ ( ( 𝐶t 𝑐 ) Homeo ( 𝐽t 𝑎 ) ) ) ) } )