Metamath Proof Explorer

Theorem unirnfdomd

Description: The union of the range of a function from an infinite set into the class of finite sets is dominated by its domain. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses unirnfdomd.1 
|- ( ph -> F : T --> Fin )
unirnfdomd.2 
|- ( ph -> -. T e. Fin )
unirnfdomd.3 
|- ( ph -> T e. V )
Assertion unirnfdomd 
|- ( ph -> U. ran F ~<_ T )

Proof

Step Hyp Ref Expression
1 unirnfdomd.1 
 |-  ( ph -> F : T --> Fin )
2 unirnfdomd.2 
 |-  ( ph -> -. T e. Fin )
3 unirnfdomd.3 
 |-  ( ph -> T e. V )
4 1 ffnd 
 |-  ( ph -> F Fn T )
5 fnex 
 |-  ( ( F Fn T /\ T e. V ) -> F e. _V )
6 4 3 5 syl2anc 
 |-  ( ph -> F e. _V )
7 rnexg 
 |-  ( F e. _V -> ran F e. _V )
8 6 7 syl 
 |-  ( ph -> ran F e. _V )
9 frn 
 |-  ( F : T --> Fin -> ran F C_ Fin )
10 dfss3 
 |-  ( ran F C_ Fin <-> A. x e. ran F x e. Fin )
11 9 10 sylib 
 |-  ( F : T --> Fin -> A. x e. ran F x e. Fin )
12 fict 
 |-  ( x e. Fin -> x ~<_ _om )
13 12 ralimi 
 |-  ( A. x e. ran F x e. Fin -> A. x e. ran F x ~<_ _om )
14 1 11 13 3syl 
 |-  ( ph -> A. x e. ran F x ~<_ _om )
15 unidom 
 |-  ( ( ran F e. _V /\ A. x e. ran F x ~<_ _om ) -> U. ran F ~<_ ( ran F X. _om ) )
16 8 14 15 syl2anc 
 |-  ( ph -> U. ran F ~<_ ( ran F X. _om ) )
17 fnrndomg 
 |-  ( T e. V -> ( F Fn T -> ran F ~<_ T ) )
18 3 4 17 sylc 
 |-  ( ph -> ran F ~<_ T )
19 omex 
 |-  _om e. _V
20 19 xpdom1 
 |-  ( ran F ~<_ T -> ( ran F X. _om ) ~<_ ( T X. _om ) )
21 18 20 syl 
 |-  ( ph -> ( ran F X. _om ) ~<_ ( T X. _om ) )
22 domtr 
 |-  ( ( U. ran F ~<_ ( ran F X. _om ) /\ ( ran F X. _om ) ~<_ ( T X. _om ) ) -> U. ran F ~<_ ( T X. _om ) )
23 16 21 22 syl2anc 
 |-  ( ph -> U. ran F ~<_ ( T X. _om ) )
24 infinf 
 |-  ( T e. V -> ( -. T e. Fin <-> _om ~<_ T ) )
25 3 24 syl 
 |-  ( ph -> ( -. T e. Fin <-> _om ~<_ T ) )
26 2 25 mpbid 
 |-  ( ph -> _om ~<_ T )
27 xpdom2g 
 |-  ( ( T e. V /\ _om ~<_ T ) -> ( T X. _om ) ~<_ ( T X. T ) )
28 3 26 27 syl2anc 
 |-  ( ph -> ( T X. _om ) ~<_ ( T X. T ) )
29 domtr 
 |-  ( ( U. ran F ~<_ ( T X. _om ) /\ ( T X. _om ) ~<_ ( T X. T ) ) -> U. ran F ~<_ ( T X. T ) )
30 23 28 29 syl2anc 
 |-  ( ph -> U. ran F ~<_ ( T X. T ) )
31 infxpidm 
 |-  ( _om ~<_ T -> ( T X. T ) ~~ T )
32 26 31 syl 
 |-  ( ph -> ( T X. T ) ~~ T )
33 domentr 
 |-  ( ( U. ran F ~<_ ( T X. T ) /\ ( T X. T ) ~~ T ) -> U. ran F ~<_ T )
34 30 32 33 syl2anc 
 |-  ( ph -> U. ran F ~<_ T )