Metamath Proof Explorer

Theorem infeq5i

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

Ref Expression
Assertion infeq5i ⊢ ω ∈ V → ∃ x x ⊂ ⋃ x

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 ⊢ x = ω ∖ ∅ → x ⊂ ⋃ x ↔ ω ∖ ∅ ⊂ ⋃ x
21 unieq ⊢ x = ω ∖ ∅ → ⋃ x = ⋃ ω ∖ ∅
22 21 psseq2d ⊢ x = ω ∖ ∅ → ω ∖ ∅ ⊂ ⋃ x ↔ ω ∖ ∅ ⊂ ⋃ ω ∖ ∅
23 20 22 bitrd ⊢ x = ω ∖ ∅ → x ⊂ ⋃ x ↔ ω ∖ ∅ ⊂ ⋃ ω ∖ ∅
24 23 spcegv ⊢ ω ∖ ∅ ∈ V → ω ∖ ∅ ⊂ ⋃ ω ∖ ∅ → ∃ x x ⊂ ⋃ x
25 1 19 24 mpisyl ⊢ ω ∈ V → ∃ x x ⊂ ⋃ x