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 sbccom
 |-  ( [. z / x ]. [. w / y ]. ph <-> [. w / y ]. [. z / x ]. ph )
24 sbceq1a
 |-  ( y = w -> ( [. z / x ]. ph <-> [. w / y ]. [. z / x ]. ph ) )
25 24 equcoms
 |-  ( w = y -> ( [. z / x ]. ph <-> [. w / y ]. [. z / x ]. ph ) )
26 23 25 bitr4id
 |-  ( 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 ) )