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

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 ( ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 ↔ ω ∈ V )

Proof

Step Hyp Ref Expression
1 df-pss ⊢ ( 𝑥 ⊊ ∪ 𝑥 ↔ ( 𝑥 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∪ 𝑥 ) )
2 unieq ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∪ ∅ )
3 uni0 ⊢ ∪ ∅ = ∅
4 2 3 eqtr2di ⊢ ( 𝑥 = ∅ → ∅ = ∪ 𝑥 )
5 eqtr ⊢ ( ( 𝑥 = ∅ ∧ ∅ = ∪ 𝑥 ) → 𝑥 = ∪ 𝑥 )
6 4 5 mpdan ⊢ ( 𝑥 = ∅ → 𝑥 = ∪ 𝑥 )
7 6 necon3i ⊢ ( 𝑥 ≠ ∪ 𝑥 → 𝑥 ≠ ∅ )
8 7 anim1i ⊢ ( ( 𝑥 ≠ ∪ 𝑥 ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) )
9 8 ancoms ⊢ ( ( 𝑥 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∪ 𝑥 ) → ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) )
10 1 9 sylbi ⊢ ( 𝑥 ⊊ ∪ 𝑥 → ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) )
11 10 eximi ⊢ ( ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 → ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) )
12 eqid ⊢ ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
13 eqid ⊢ ( rec ( ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) , ∅ ) ↾ ω )
14 vex ⊢ 𝑥 ∈ V
15 12 13 14 14 inf3lem7 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ω ∈ V )
16 15 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ω ∈ V )
17 11 16 syl ⊢ ( ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 → ω ∈ V )
18 infeq5i ⊢ ( ω ∈ V → ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 )
19 17 18 impbii ⊢ ( ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 ↔ ω ∈ V )