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 )