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