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

Metamath Proof Explorer

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