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 e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
Assertion cvmscbv 
|- S = ( a e. J |-> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 iscvm.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 unieq 
 |-  ( s = b -> U. s = U. b )
3 2 eqeq1d 
 |-  ( s = b -> ( U. s = ( `' F " k ) <-> U. b = ( `' F " k ) ) )
4 ineq2 
 |-  ( v = d -> ( u i^i v ) = ( u i^i d ) )
5 4 eqeq1d 
 |-  ( v = d -> ( ( u i^i v ) = (/) <-> ( u i^i d ) = (/) ) )
6 5 cbvralvw 
 |-  ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) <-> A. d e. ( s \ { u } ) ( u i^i d ) = (/) )
7 sneq 
 |-  ( u = c -> { u } = { c } )
8 7 difeq2d 
 |-  ( u = c -> ( s \ { u } ) = ( s \ { c } ) )
9 ineq1 
 |-  ( u = c -> ( u i^i d ) = ( c i^i d ) )
10 9 eqeq1d 
 |-  ( u = c -> ( ( u i^i d ) = (/) <-> ( c i^i d ) = (/) ) )
11 8 10 raleqbidv 
 |-  ( u = c -> ( A. d e. ( s \ { u } ) ( u i^i d ) = (/) <-> A. d e. ( s \ { c } ) ( c i^i d ) = (/) ) )
12 6 11 syl5bb 
 |-  ( u = c -> ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) <-> A. d e. ( s \ { c } ) ( c i^i d ) = (/) ) )
13 reseq2 
 |-  ( u = c -> ( F |` u ) = ( F |` c ) )
14 oveq2 
 |-  ( u = c -> ( C |`t u ) = ( C |`t c ) )
15 14 oveq1d 
 |-  ( u = c -> ( ( C |`t u ) Homeo ( J |`t k ) ) = ( ( C |`t c ) Homeo ( J |`t k ) ) )
16 13 15 eleq12d 
 |-  ( u = c -> ( ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) <-> ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) )
17 12 16 anbi12d 
 |-  ( u = c -> ( ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) <-> ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) )
18 17 cbvralvw 
 |-  ( A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) <-> A. c e. s ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) )
19 difeq1 
 |-  ( s = b -> ( s \ { c } ) = ( b \ { c } ) )
20 19 raleqdv 
 |-  ( s = b -> ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) <-> A. d e. ( b \ { c } ) ( c i^i d ) = (/) ) )
21 20 anbi1d 
 |-  ( s = b -> ( ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) <-> ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) )
22 21 raleqbi1dv 
 |-  ( s = b -> ( A. c e. s ( A. d e. ( s \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) <-> A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) )
23 18 22 syl5bb 
 |-  ( s = b -> ( A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) <-> A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) )
24 3 23 anbi12d 
 |-  ( s = b -> ( ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) <-> ( U. b = ( `' F " k ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) ) )
25 24 cbvrabv 
 |-  { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } = { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " k ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) }
26 imaeq2 
 |-  ( k = a -> ( `' F " k ) = ( `' F " a ) )
27 26 eqeq2d 
 |-  ( k = a -> ( U. b = ( `' F " k ) <-> U. b = ( `' F " a ) ) )
28 oveq2 
 |-  ( k = a -> ( J |`t k ) = ( J |`t a ) )
29 28 oveq2d 
 |-  ( k = a -> ( ( C |`t c ) Homeo ( J |`t k ) ) = ( ( C |`t c ) Homeo ( J |`t a ) ) )
30 29 eleq2d 
 |-  ( k = a -> ( ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) <-> ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) )
31 30 anbi2d 
 |-  ( k = a -> ( ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) <-> ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) )
32 31 ralbidv 
 |-  ( k = a -> ( A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) <-> A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) )
33 27 32 anbi12d 
 |-  ( k = a -> ( ( U. b = ( `' F " k ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) <-> ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) ) )
34 33 rabbidv 
 |-  ( k = a -> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " k ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t k ) ) ) ) } = { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) } )
35 25 34 syl5eq 
 |-  ( k = a -> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } = { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) } )
36 35 cbvmptv 
 |-  ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } ) = ( a e. J |-> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) } )
37 1 36 eqtri 
 |-  S = ( a e. J |-> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) } )