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

Metamath Proof Explorer

Theorem abnex

Description: Sufficient condition for a class abstraction to be a proper class. Lemma for snnex and pwnex . See the comment of abnexg . (Contributed by BJ, 2-May-2021)

		Ref	Expression
	Assertion	abnex	⊢ ( ∀ 𝑥 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ¬ { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝐹 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		vprc	⊢ ¬ V ∈ V
2		alral	⊢ ( ∀ 𝑥 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ∀ 𝑥 ∈ V ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) )
3		rexv	⊢ ( ∃ 𝑥 ∈ V 𝑦 = 𝐹 ↔ ∃ 𝑥 𝑦 = 𝐹 )
4	3	bicomi	⊢ ( ∃ 𝑥 𝑦 = 𝐹 ↔ ∃ 𝑥 ∈ V 𝑦 = 𝐹 )
5	4	abbii	⊢ { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝐹 } = { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = 𝐹 }
6	5	eleq1i	⊢ ( { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝐹 } ∈ V ↔ { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = 𝐹 } ∈ V )
7	6	biimpi	⊢ ( { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝐹 } ∈ V → { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = 𝐹 } ∈ V )
8		abnexg	⊢ ( ∀ 𝑥 ∈ V ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ( { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = 𝐹 } ∈ V → V ∈ V ) )
9	2 7 8	syl2im	⊢ ( ∀ 𝑥 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ( { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝐹 } ∈ V → V ∈ V ) )
10	1 9	mtoi	⊢ ( ∀ 𝑥 ( 𝐹 ∈ 𝑉 ∧ 𝑥 ∈ 𝐹 ) → ¬ { 𝑦 ∣ ∃ 𝑥 𝑦 = 𝐹 } ∈ V )