Theorem abnexg

Description: Sufficient condition for a class abstraction to be a proper class. The class F can be thought of as an expression in x and the abstraction appearing in the statement as the class of values F as x varies through A . Assuming the antecedents, if that class is a set, then so is the "domain" A . The converse holds without antecedent, see abrexexg . Note that the second antecedent A. x e. A x e. F cannot be translated to A C_ F since F may depend on x . In applications, one may take F = { x } or F = ~P x (see snnex and pwnex respectively, proved from abnex , which is a consequence of abnexg with A = _V ). (Contributed by BJ, 2-Dec-2021)

	Ref	Expression
Assertion	abnexg	|- ( A. x e. A ( F e. V /\ x e. F ) -> ( { y | E. x e. A y = F } e. W -> A e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		uniexg	|- ( { y | E. x e. A y = F } e. W -> U. { y | E. x e. A y = F } e. _V )
2		simpl	|- ( ( F e. V /\ x e. F ) -> F e. V )
3	2	ralimi	|- ( A. x e. A ( F e. V /\ x e. F ) -> A. x e. A F e. V )
4		dfiun2g	|- ( A. x e. A F e. V -> U_ x e. A F = U. { y | E. x e. A y = F } )
5	4	eleq1d	|- ( A. x e. A F e. V -> ( U_ x e. A F e. _V <-> U. { y | E. x e. A y = F } e. _V ) )
6	5	biimprd	|- ( A. x e. A F e. V -> ( U. { y | E. x e. A y = F } e. _V -> U_ x e. A F e. _V ) )
7	3 6	syl	|- ( A. x e. A ( F e. V /\ x e. F ) -> ( U. { y | E. x e. A y = F } e. _V -> U_ x e. A F e. _V ) )
8		simpr	|- ( ( F e. V /\ x e. F ) -> x e. F )
9	8	ralimi	|- ( A. x e. A ( F e. V /\ x e. F ) -> A. x e. A x e. F )
10		iunid	|- U_ x e. A { x } = A
11		snssi	|- ( x e. F -> { x } C_ F )
12	11	ralimi	|- ( A. x e. A x e. F -> A. x e. A { x } C_ F )
13		ss2iun	|- ( A. x e. A { x } C_ F -> U_ x e. A { x } C_ U_ x e. A F )
14	12 13	syl	|- ( A. x e. A x e. F -> U_ x e. A { x } C_ U_ x e. A F )
15	10 14	eqsstrrid	|- ( A. x e. A x e. F -> A C_ U_ x e. A F )
16		ssexg	|- ( ( A C_ U_ x e. A F /\ U_ x e. A F e. _V ) -> A e. _V )
17	16	ex	|- ( A C_ U_ x e. A F -> ( U_ x e. A F e. _V -> A e. _V ) )
18	9 15 17	3syl	|- ( A. x e. A ( F e. V /\ x e. F ) -> ( U_ x e. A F e. _V -> A e. _V ) )
19	7 18	syld	|- ( A. x e. A ( F e. V /\ x e. F ) -> ( U. { y | E. x e. A y = F } e. _V -> A e. _V ) )
20	1 19	syl5	|- ( A. x e. A ( F e. V /\ x e. F ) -> ( { y | E. x e. A y = F } e. W -> A e. _V ) )