Metamath Proof Explorer

Theorem dominf

Description: A nonempty set that is a subset of its union is infinite. This version is proved from ax-cc . See dominfac for a version proved from ax-ac . The axiom of Regularity is used for this proof, via inf3lem6 , and its use is necessary: otherwise the set A = { A } or A = { (/) , A } (where the second example even has nonempty well-founded part) provides a counterexample. (Contributed by Mario Carneiro, 9-Feb-2013)

Ref Expression
Hypothesis dominf.1 
|- A e. _V
Assertion dominf 
|- ( ( A =/= (/) /\ A C_ U. A ) -> _om ~<_ A )

Proof

Step Hyp Ref Expression
1 dominf.1 
 |-  A e. _V
2 neeq1 
 |-  ( x = A -> ( x =/= (/) <-> A =/= (/) ) )
3 id 
 |-  ( x = A -> x = A )
4 unieq 
 |-  ( x = A -> U. x = U. A )
5 3 4 sseq12d 
 |-  ( x = A -> ( x C_ U. x <-> A C_ U. A ) )
6 2 5 anbi12d 
 |-  ( x = A -> ( ( x =/= (/) /\ x C_ U. x ) <-> ( A =/= (/) /\ A C_ U. A ) ) )
7 breq2 
 |-  ( x = A -> ( _om ~<_ x <-> _om ~<_ A ) )
8 6 7 imbi12d 
 |-  ( x = A -> ( ( ( x =/= (/) /\ x C_ U. x ) -> _om ~<_ x ) <-> ( ( A =/= (/) /\ A C_ U. A ) -> _om ~<_ A ) ) )
9 eqid 
 |-  ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) = ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } )
10 eqid 
 |-  ( rec ( ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) , (/) ) |` _om ) = ( rec ( ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) , (/) ) |` _om )
11 9 10 1 1 inf3lem6 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> ( rec ( ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) , (/) ) |` _om ) : _om -1-1-> ~P x )
12 vpwex 
 |-  ~P x e. _V
13 12 f1dom 
 |-  ( ( rec ( ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) , (/) ) |` _om ) : _om -1-1-> ~P x -> _om ~<_ ~P x )
14 pwfi 
 |-  ( x e. Fin <-> ~P x e. Fin )
15 14 biimpi 
 |-  ( x e. Fin -> ~P x e. Fin )
16 isfinite 
 |-  ( x e. Fin <-> x ~< _om )
17 isfinite 
 |-  ( ~P x e. Fin <-> ~P x ~< _om )
18 15 16 17 3imtr3i 
 |-  ( x ~< _om -> ~P x ~< _om )
19 18 con3i 
 |-  ( -. ~P x ~< _om -> -. x ~< _om )
20 12 domtriom 
 |-  ( _om ~<_ ~P x <-> -. ~P x ~< _om )
21 vex 
 |-  x e. _V
22 21 domtriom 
 |-  ( _om ~<_ x <-> -. x ~< _om )
23 19 20 22 3imtr4i 
 |-  ( _om ~<_ ~P x -> _om ~<_ x )
24 11 13 23 3syl 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> _om ~<_ x )
25 1 8 24 vtocl 
 |-  ( ( A =/= (/) /\ A C_ U. A ) -> _om ~<_ A )