Metamath Proof Explorer


Theorem infeq5

Description: The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (shown on the right-hand side in the form of omex .) The left-hand side provides us with a very short way to express the Axiom of Infinity using only elementary symbols. This proof of equivalence does not depend on the Axiom of Infinity. (Contributed by NM, 23-Mar-2004) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion infeq5 x x x ω V

Proof

Step Hyp Ref Expression
1 df-pss x x x x x x
2 unieq x = x =
3 uni0 =
4 2 3 eqtr2di x = = x
5 eqtr x = = x x = x
6 4 5 mpdan x = x = x
7 6 necon3i x x x
8 7 anim1i x x x x x x x
9 8 ancoms x x x x x x x
10 1 9 sylbi x x x x x
11 10 eximi x x x x x x x
12 eqid y V w x | w x y = y V w x | w x y
13 eqid rec y V w x | w x y ω = rec y V w x | w x y ω
14 vex x V
15 12 13 14 14 inf3lem7 x x x ω V
16 15 exlimiv x x x x ω V
17 11 16 syl x x x ω V
18 infeq5i ω V x x x
19 17 18 impbii x x x ω V