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

Metamath Proof Explorer

Theorem infeq5i

Description: Half of infeq5 . (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion infeq5i ( ω ∈ V → ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 )

Proof

Step Hyp Ref Expression
1 difexg ⊢ ( ω ∈ V → ( ω ∖ { ∅ } ) ∈ V )
2 0ex ⊢ ∅ ∈ V
3 2 snid ⊢ ∅ ∈ { ∅ }
4 disj4 ⊢ ( ( ω ∩ { ∅ } ) = ∅ ↔ ¬ ( ω ∖ { ∅ } ) ⊊ ω )
5 disj3 ⊢ ( ( ω ∩ { ∅ } ) = ∅ ↔ ω = ( ω ∖ { ∅ } ) )
6 4 5 bitr3i ⊢ ( ¬ ( ω ∖ { ∅ } ) ⊊ ω ↔ ω = ( ω ∖ { ∅ } ) )
7 peano1 ⊢ ∅ ∈ ω
8 eleq2 ⊢ ( ω = ( ω ∖ { ∅ } ) → ( ∅ ∈ ω ↔ ∅ ∈ ( ω ∖ { ∅ } ) ) )
9 7 8 mpbii ⊢ ( ω = ( ω ∖ { ∅ } ) → ∅ ∈ ( ω ∖ { ∅ } ) )
10 9 eldifbd ⊢ ( ω = ( ω ∖ { ∅ } ) → ¬ ∅ ∈ { ∅ } )
11 6 10 sylbi ⊢ ( ¬ ( ω ∖ { ∅ } ) ⊊ ω → ¬ ∅ ∈ { ∅ } )
12 3 11 mt4 ⊢ ( ω ∖ { ∅ } ) ⊊ ω
13 unidif0 ⊢ ∪ ( ω ∖ { ∅ } ) = ∪ ω
14 limom ⊢ Lim ω
15 limuni ⊢ ( Lim ω → ω = ∪ ω )
16 14 15 ax-mp ⊢ ω = ∪ ω
17 13 16 eqtr4i ⊢ ∪ ( ω ∖ { ∅ } ) = ω
18 17 psseq2i ⊢ ( ( ω ∖ { ∅ } ) ⊊ ∪ ( ω ∖ { ∅ } ) ↔ ( ω ∖ { ∅ } ) ⊊ ω )
19 12 18 mpbir ⊢ ( ω ∖ { ∅ } ) ⊊ ∪ ( ω ∖ { ∅ } )
20 psseq1 ⊢ ( 𝑥 = ( ω ∖ { ∅ } ) → ( 𝑥 ⊊ ∪ 𝑥 ↔ ( ω ∖ { ∅ } ) ⊊ ∪ 𝑥 ) )
21 unieq ⊢ ( 𝑥 = ( ω ∖ { ∅ } ) → ∪ 𝑥 = ∪ ( ω ∖ { ∅ } ) )
22 21 psseq2d ⊢ ( 𝑥 = ( ω ∖ { ∅ } ) → ( ( ω ∖ { ∅ } ) ⊊ ∪ 𝑥 ↔ ( ω ∖ { ∅ } ) ⊊ ∪ ( ω ∖ { ∅ } ) ) )
23 20 22 bitrd ⊢ ( 𝑥 = ( ω ∖ { ∅ } ) → ( 𝑥 ⊊ ∪ 𝑥 ↔ ( ω ∖ { ∅ } ) ⊊ ∪ ( ω ∖ { ∅ } ) ) )
24 23 spcegv ⊢ ( ( ω ∖ { ∅ } ) ∈ V → ( ( ω ∖ { ∅ } ) ⊊ ∪ ( ω ∖ { ∅ } ) → ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 ) )
25 1 19 24 mpisyl ⊢ ( ω ∈ V → ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 )