Theorem fiprc

Description: The class of finite sets is a proper class. (Contributed by Jeff Hankins, 3-Oct-2008)

	Ref	Expression
Assertion	fiprc	⊢ Fin ∉ V

Proof

Step	Hyp	Ref	Expression
1		snnex	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∉ V
2		snfi	⊢ { 𝑦 } ∈ Fin
3		eleq1	⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ∈ Fin ↔ { 𝑦 } ∈ Fin ) )
4	2 3	mpbiri	⊢ ( 𝑥 = { 𝑦 } → 𝑥 ∈ Fin )
5	4	exlimiv	⊢ ( ∃ 𝑦 𝑥 = { 𝑦 } → 𝑥 ∈ Fin )
6	5	abssi	⊢ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ⊆ Fin
7		ssexg	⊢ ( ( { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ⊆ Fin ∧ Fin ∈ V ) → { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∈ V )
8	6 7	mpan	⊢ ( Fin ∈ V → { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∈ V )
9	8	con3i	⊢ ( ¬ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∈ V → ¬ Fin ∈ V )
10		df-nel	⊢ ( { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∉ V ↔ ¬ { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∈ V )
11		df-nel	⊢ ( Fin ∉ V ↔ ¬ Fin ∈ V )
12	9 10 11	3imtr4i	⊢ ( { 𝑥 ∣ ∃ 𝑦 𝑥 = { 𝑦 } } ∉ V → Fin ∉ V )
13	1 12	ax-mp	⊢ Fin ∉ V