Metamath Proof Explorer

Theorem dominfac

Description: A nonempty set that is a subset of its union is infinite. This version is proved from ax-ac . See dominf for a version proved from ax-cc . (Contributed by NM, 25-Mar-2007)

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

Proof

Step Hyp Ref Expression
1 dominfac.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 omex 
 |-  _om e. _V
21 domtri 
 |-  ( ( _om e. _V /\ ~P x e. _V ) -> ( _om ~<_ ~P x <-> -. ~P x ~< _om ) )
22 20 12 21 mp2an 
 |-  ( _om ~<_ ~P x <-> -. ~P x ~< _om )
23 vex 
 |-  x e. _V
24 domtri 
 |-  ( ( _om e. _V /\ x e. _V ) -> ( _om ~<_ x <-> -. x ~< _om ) )
25 20 23 24 mp2an 
 |-  ( _om ~<_ x <-> -. x ~< _om )
26 19 22 25 3imtr4i 
 |-  ( _om ~<_ ~P x -> _om ~<_ x )
27 11 13 26 3syl 
 |-  ( ( x =/= (/) /\ x C_ U. x ) -> _om ~<_ x )
28 1 8 27 vtocl 
 |-  ( ( A =/= (/) /\ A C_ U. A ) -> _om ~<_ A )