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	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ 𝑊 → 𝐴 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ 𝑊 → ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ V )
2		simpl	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → 𝐹 ∈ 𝑉 )
3	2	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ∀ 𝑥 ∈ 𝐴 𝐹 ∈ 𝑉 )
4		dfiun2g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐹 ∈ 𝑉 → ∪ 𝑥 ∈ 𝐴 𝐹 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } )
5	4	eleq1d	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐹 ∈ 𝑉 → ( ∪ 𝑥 ∈ 𝐴 𝐹 ∈ V ↔ ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ V ) )
6	5	biimprd	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐹 ∈ 𝑉 → ( ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ V → ∪ 𝑥 ∈ 𝐴 𝐹 ∈ V ) )
7	3 6	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ( ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ V → ∪ 𝑥 ∈ 𝐴 𝐹 ∈ V ) )
8		simpr	⊢ ( ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → 𝑥 ∈ 𝐹 )
9	8	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐹 )
10		iunid	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴
11		snssi	⊢ ( 𝑥 ∈ 𝐹 → { 𝑥 } ⊆ 𝐹 )
12	11	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐹 → ∀ 𝑥 ∈ 𝐴 { 𝑥 } ⊆ 𝐹 )
13		ss2iun	⊢ ( ∀ 𝑥 ∈ 𝐴 { 𝑥 } ⊆ 𝐹 → ∪ 𝑥 ∈ 𝐴 { 𝑥 } ⊆ ∪ 𝑥 ∈ 𝐴 𝐹 )
14	12 13	syl	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐹 → ∪ 𝑥 ∈ 𝐴 { 𝑥 } ⊆ ∪ 𝑥 ∈ 𝐴 𝐹 )
15	10 14	eqsstrrid	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐹 → 𝐴 ⊆ ∪ 𝑥 ∈ 𝐴 𝐹 )
16		ssexg	⊢ ( ( 𝐴 ⊆ ∪ 𝑥 ∈ 𝐴 𝐹 ∧ ∪ 𝑥 ∈ 𝐴 𝐹 ∈ V ) → 𝐴 ∈ V )
17	16	ex	⊢ ( 𝐴 ⊆ ∪ 𝑥 ∈ 𝐴 𝐹 → ( ∪ 𝑥 ∈ 𝐴 𝐹 ∈ V → 𝐴 ∈ V ) )
18	9 15 17	3syl	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ( ∪ 𝑥 ∈ 𝐴 𝐹 ∈ V → 𝐴 ∈ V ) )
19	7 18	syld	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ( ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ V → 𝐴 ∈ V ) )
20	1 19	syl5	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐹 } ∈ 𝑊 → 𝐴 ∈ V ) )