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 → ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 )