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 )

Metamath Proof Explorer

Theorem bnj1366

Proof