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	$⊢ \forall x \in A (F \in V \land x \in F) \to (\{y \| \exists x \in A y = F\} \in W \to A \in V)$

Proof

Step	Hyp	Ref	Expression
1		uniexg	$⊢ \{y \| \exists x \in A y = F\} \in W \to ⋃ \{y \| \exists x \in A y = F\} \in V$
2		simpl	$⊢ (F \in V \land x \in F) \to F \in V$
3	2	ralimi	$⊢ \forall x \in A (F \in V \land x \in F) \to \forall x \in A F \in V$
4		dfiun2g	$⊢ \forall x \in A F \in V \to ⋃_{x \in A} F = ⋃ \{y \| \exists x \in A y = F\}$
5	4	eleq1d	$⊢ \forall x \in A F \in V \to (⋃_{x \in A} F \in V \leftrightarrow ⋃ \{y \| \exists x \in A y = F\} \in V)$
6	5	biimprd	$⊢ \forall x \in A F \in V \to (⋃ \{y \| \exists x \in A y = F\} \in V \to ⋃_{x \in A} F \in V)$
7	3 6	syl	$⊢ \forall x \in A (F \in V \land x \in F) \to (⋃ \{y \| \exists x \in A y = F\} \in V \to ⋃_{x \in A} F \in V)$
8		simpr	$⊢ (F \in V \land x \in F) \to x \in F$
9	8	ralimi	$⊢ \forall x \in A (F \in V \land x \in F) \to \forall x \in A x \in F$
10		iunid	$⊢ ⋃_{x \in A} \{x\} = A$
11		snssi	$⊢ x \in F \to \{x\} \subseteq F$
12	11	ralimi	$⊢ \forall x \in A x \in F \to \forall x \in A \{x\} \subseteq F$
13		ss2iun	$⊢ \forall x \in A \{x\} \subseteq F \to ⋃_{x \in A} \{x\} \subseteq ⋃_{x \in A} F$
14	12 13	syl	$⊢ \forall x \in A x \in F \to ⋃_{x \in A} \{x\} \subseteq ⋃_{x \in A} F$
15	10 14	eqsstrrid	$⊢ \forall x \in A x \in F \to A \subseteq ⋃_{x \in A} F$
16		ssexg	$⊢ (A \subseteq ⋃_{x \in A} F \land ⋃_{x \in A} F \in V) \to A \in V$
17	16	ex	$⊢ A \subseteq ⋃_{x \in A} F \to (⋃_{x \in A} F \in V \to A \in V)$
18	9 15 17	3syl	$⊢ \forall x \in A (F \in V \land x \in F) \to (⋃_{x \in A} F \in V \to A \in V)$
19	7 18	syld	$⊢ \forall x \in A (F \in V \land x \in F) \to (⋃ \{y \| \exists x \in A y = F\} \in V \to A \in V)$
20	1 19	syl5	$⊢ \forall x \in A (F \in V \land x \in F) \to (\{y \| \exists x \in A y = F\} \in W \to A \in V)$

Metamath Proof Explorer

Theorem abnexg

Proof