This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )