Metamath Proof Explorer


Theorem bnj1366

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1366.1
|- ( ps <-> ( A e. _V /\ A. x e. A E! y ph /\ B = { y | E. x e. A ph } ) )
Assertion bnj1366
|- ( ps -> B e. _V )

Proof

Step Hyp Ref Expression
1 bnj1366.1
 |-  ( ps <-> ( A e. _V /\ A. x e. A E! y ph /\ B = { y | E. x e. A ph } ) )
2 1 simp3bi
 |-  ( ps -> B = { y | E. x e. A ph } )
3 1 simp2bi
 |-  ( ps -> A. x e. A E! y ph )
4 nfcv
 |-  F/_ y A
5 nfeu1
 |-  F/ y E! y ph
6 4 5 nfralw
 |-  F/ y A. x e. A E! y ph
7 nfra1
 |-  F/ x A. x e. A E! y ph
8 rspa
 |-  ( ( A. x e. A E! y ph /\ x e. A ) -> E! y ph )
9 iota1
 |-  ( E! y ph -> ( ph <-> ( iota y ph ) = y ) )
10 eqcom
 |-  ( ( iota y ph ) = y <-> y = ( iota y ph ) )
11 9 10 bitrdi
 |-  ( E! y ph -> ( ph <-> y = ( iota y ph ) ) )
12 8 11 syl
 |-  ( ( A. x e. A E! y ph /\ x e. A ) -> ( ph <-> y = ( iota y ph ) ) )
13 7 12 rexbida
 |-  ( A. x e. A E! y ph -> ( E. x e. A ph <-> E. x e. A y = ( iota y ph ) ) )
14 abid
 |-  ( y e. { y | E. x e. A ph } <-> E. x e. A ph )
15 eqid
 |-  ( x e. A |-> ( iota y ph ) ) = ( x e. A |-> ( iota y ph ) )
16 iotaex
 |-  ( iota y ph ) e. _V
17 15 16 elrnmpti
 |-  ( y e. ran ( x e. A |-> ( iota y ph ) ) <-> E. x e. A y = ( iota y ph ) )
18 13 14 17 3bitr4g
 |-  ( A. x e. A E! y ph -> ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
19 6 18 alrimi
 |-  ( A. x e. A E! y ph -> A. y ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
20 3 19 syl
 |-  ( ps -> A. y ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
21 nfab1
 |-  F/_ y { y | E. x e. A ph }
22 nfiota1
 |-  F/_ y ( iota y ph )
23 4 22 nfmpt
 |-  F/_ y ( x e. A |-> ( iota y ph ) )
24 23 nfrn
 |-  F/_ y ran ( x e. A |-> ( iota y ph ) )
25 21 24 cleqf
 |-  ( { y | E. x e. A ph } = ran ( x e. A |-> ( iota y ph ) ) <-> A. y ( y e. { y | E. x e. A ph } <-> y e. ran ( x e. A |-> ( iota y ph ) ) ) )
26 20 25 sylibr
 |-  ( ps -> { y | E. x e. A ph } = ran ( x e. A |-> ( iota y ph ) ) )
27 2 26 eqtrd
 |-  ( ps -> B = ran ( x e. A |-> ( iota y ph ) ) )
28 1 simp1bi
 |-  ( ps -> A e. _V )
29 mptexg
 |-  ( A e. _V -> ( x e. A |-> ( iota y ph ) ) e. _V )
30 rnexg
 |-  ( ( x e. A |-> ( iota y ph ) ) e. _V -> ran ( x e. A |-> ( iota y ph ) ) e. _V )
31 28 29 30 3syl
 |-  ( ps -> ran ( x e. A |-> ( iota y ph ) ) e. _V )
32 27 31 eqeltrd
 |-  ( ps -> B e. _V )