Metamath Proof Explorer

Theorem elmptrab

Description: Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Hypotheses elmptrab.f 
|- F = ( x e. D |-> { y e. B | ph } )
elmptrab.s1 
|- ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
elmptrab.s2 
|- ( x = X -> B = C )
elmptrab.ex 
|- ( x e. D -> B e. V )
Assertion elmptrab 
|- ( Y e. ( F ` X ) <-> ( X e. D /\ Y e. C /\ ps ) )

Proof

Step Hyp Ref Expression
1 elmptrab.f 
 |-  F = ( x e. D |-> { y e. B | ph } )
2 elmptrab.s1 
 |-  ( ( x = X /\ y = Y ) -> ( ph <-> ps ) )
3 elmptrab.s2 
 |-  ( x = X -> B = C )
4 elmptrab.ex 
 |-  ( x e. D -> B e. V )
5 1 mptrcl 
 |-  ( Y e. ( F ` X ) -> X e. D )
6 simp1 
 |-  ( ( X e. D /\ Y e. C /\ ps ) -> X e. D )
7 csbeq1 
 |-  ( z = X -> [_ z / x ]_ B = [_ X / x ]_ B )
8 dfsbcq 
 |-  ( z = X -> ( [. z / x ]. [. w / y ]. ph <-> [. X / x ]. [. w / y ]. ph ) )
9 7 8 rabeqbidv 
 |-  ( z = X -> { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph } = { w e. [_ X / x ]_ B | [. X / x ]. [. w / y ]. ph } )
10 nfcv 
 |-  F/_ z { y e. B | ph }
11 nfsbc1v 
 |-  F/ x [. z / x ]. [. w / y ]. ph
12 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
13 11 12 nfrabw 
 |-  F/_ x { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph }
14 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
15 sbceq1a 
 |-  ( x = z -> ( ph <-> [. z / x ]. ph ) )
16 14 15 rabeqbidv 
 |-  ( x = z -> { y e. B | ph } = { y e. [_ z / x ]_ B | [. z / x ]. ph } )
17 nfcv 
 |-  F/_ w [_ z / x ]_ B
18 nfcv 
 |-  F/_ y [_ z / x ]_ B
19 nfcv 
 |-  F/_ y z
20 nfsbc1v 
 |-  F/ y [. w / y ]. ph
21 19 20 nfsbcw 
 |-  F/ y [. z / x ]. [. w / y ]. ph
22 nfv 
 |-  F/ w [. z / x ]. ph
23 sbceq1a 
 |-  ( y = w -> ( [. z / x ]. ph <-> [. w / y ]. [. z / x ]. ph ) )
24 23 equcoms 
 |-  ( w = y -> ( [. z / x ]. ph <-> [. w / y ]. [. z / x ]. ph ) )
25 sbccom 
 |-  ( [. z / x ]. [. w / y ]. ph <-> [. w / y ]. [. z / x ]. ph )
26 24 25 syl6rbbr 
 |-  ( w = y -> ( [. z / x ]. [. w / y ]. ph <-> [. z / x ]. ph ) )
27 17 18 21 22 26 cbvrabw 
 |-  { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph } = { y e. [_ z / x ]_ B | [. z / x ]. ph }
28 16 27 eqtr4di 
 |-  ( x = z -> { y e. B | ph } = { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph } )
29 10 13 28 cbvmpt 
 |-  ( x e. D |-> { y e. B | ph } ) = ( z e. D |-> { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph } )
30 1 29 eqtri 
 |-  F = ( z e. D |-> { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph } )
31 nfv 
 |-  F/ x z e. D
32 12 nfel1 
 |-  F/ x [_ z / x ]_ B e. V
33 31 32 nfim 
 |-  F/ x ( z e. D -> [_ z / x ]_ B e. V )
34 eleq1w 
 |-  ( x = z -> ( x e. D <-> z e. D ) )
35 14 eleq1d 
 |-  ( x = z -> ( B e. V <-> [_ z / x ]_ B e. V ) )
36 34 35 imbi12d 
 |-  ( x = z -> ( ( x e. D -> B e. V ) <-> ( z e. D -> [_ z / x ]_ B e. V ) ) )
37 33 36 4 chvarfv 
 |-  ( z e. D -> [_ z / x ]_ B e. V )
38 rabexg 
 |-  ( [_ z / x ]_ B e. V -> { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph } e. _V )
39 37 38 syl 
 |-  ( z e. D -> { w e. [_ z / x ]_ B | [. z / x ]. [. w / y ]. ph } e. _V )
40 9 30 39 fvmpt3 
 |-  ( X e. D -> ( F ` X ) = { w e. [_ X / x ]_ B | [. X / x ]. [. w / y ]. ph } )
41 40 eleq2d 
 |-  ( X e. D -> ( Y e. ( F ` X ) <-> Y e. { w e. [_ X / x ]_ B | [. X / x ]. [. w / y ]. ph } ) )
42 dfsbcq 
 |-  ( w = Y -> ( [. w / y ]. ph <-> [. Y / y ]. ph ) )
43 42 sbcbidv 
 |-  ( w = Y -> ( [. X / x ]. [. w / y ]. ph <-> [. X / x ]. [. Y / y ]. ph ) )
44 43 elrab 
 |-  ( Y e. { w e. [_ X / x ]_ B | [. X / x ]. [. w / y ]. ph } <-> ( Y e. [_ X / x ]_ B /\ [. X / x ]. [. Y / y ]. ph ) )
45 44 a1i 
 |-  ( X e. D -> ( Y e. { w e. [_ X / x ]_ B | [. X / x ]. [. w / y ]. ph } <-> ( Y e. [_ X / x ]_ B /\ [. X / x ]. [. Y / y ]. ph ) ) )
46 nfcvd 
 |-  ( X e. D -> F/_ x C )
47 46 3 csbiegf 
 |-  ( X e. D -> [_ X / x ]_ B = C )
48 47 eleq2d 
 |-  ( X e. D -> ( Y e. [_ X / x ]_ B <-> Y e. C ) )
49 48 anbi1d 
 |-  ( X e. D -> ( ( Y e. [_ X / x ]_ B /\ [. X / x ]. [. Y / y ]. ph ) <-> ( Y e. C /\ [. X / x ]. [. Y / y ]. ph ) ) )
50 nfv 
 |-  F/ x ps
51 nfv 
 |-  F/ y ps
52 nfv 
 |-  F/ x Y e. C
53 50 51 52 2 sbc2iegf 
 |-  ( ( X e. D /\ Y e. C ) -> ( [. X / x ]. [. Y / y ]. ph <-> ps ) )
54 53 pm5.32da 
 |-  ( X e. D -> ( ( Y e. C /\ [. X / x ]. [. Y / y ]. ph ) <-> ( Y e. C /\ ps ) ) )
55 45 49 54 3bitrd 
 |-  ( X e. D -> ( Y e. { w e. [_ X / x ]_ B | [. X / x ]. [. w / y ]. ph } <-> ( Y e. C /\ ps ) ) )
56 3anass 
 |-  ( ( X e. D /\ Y e. C /\ ps ) <-> ( X e. D /\ ( Y e. C /\ ps ) ) )
57 56 baibr 
 |-  ( X e. D -> ( ( Y e. C /\ ps ) <-> ( X e. D /\ Y e. C /\ ps ) ) )
58 41 55 57 3bitrd 
 |-  ( X e. D -> ( Y e. ( F ` X ) <-> ( X e. D /\ Y e. C /\ ps ) ) )
59 5 6 58 pm5.21nii 
 |-  ( Y e. ( F ` X ) <-> ( X e. D /\ Y e. C /\ ps ) )