Metamath Proof Explorer

Theorem fsuppmapnn0fiublem

Description: Lemma for fsuppmapnn0fiub and fsuppmapnn0fiubex . (Contributed by AV, 2-Oct-2019)

Ref Expression
Hypotheses fsuppmapnn0fiub.u 
|- U = U_ f e. M ( f supp Z )
fsuppmapnn0fiub.s 
|- S = sup ( U , RR , < )
Assertion fsuppmapnn0fiublem 
|- ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( ( A. f e. M f finSupp Z /\ U =/= (/) ) -> S e. NN0 ) )

Proof

Step Hyp Ref Expression
1 fsuppmapnn0fiub.u 
 |-  U = U_ f e. M ( f supp Z )
2 fsuppmapnn0fiub.s 
 |-  S = sup ( U , RR , < )
3 nfv 
 |-  F/ f ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V )
4 nfra1 
 |-  F/ f A. f e. M f finSupp Z
5 nfv 
 |-  F/ f U =/= (/)
6 4 5 nfan 
 |-  F/ f ( A. f e. M f finSupp Z /\ U =/= (/) )
7 3 6 nfan 
 |-  F/ f ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) )
8 suppssdm 
 |-  ( f supp Z ) C_ dom f
9 ssel2 
 |-  ( ( M C_ ( R ^m NN0 ) /\ f e. M ) -> f e. ( R ^m NN0 ) )
10 elmapfn 
 |-  ( f e. ( R ^m NN0 ) -> f Fn NN0 )
11 fndm 
 |-  ( f Fn NN0 -> dom f = NN0 )
12 eqimss 
 |-  ( dom f = NN0 -> dom f C_ NN0 )
13 11 12 syl 
 |-  ( f Fn NN0 -> dom f C_ NN0 )
14 9 10 13 3syl 
 |-  ( ( M C_ ( R ^m NN0 ) /\ f e. M ) -> dom f C_ NN0 )
15 14 ex 
 |-  ( M C_ ( R ^m NN0 ) -> ( f e. M -> dom f C_ NN0 ) )
16 15 3ad2ant1 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( f e. M -> dom f C_ NN0 ) )
17 16 adantr 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( f e. M -> dom f C_ NN0 ) )
18 17 imp 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> dom f C_ NN0 )
19 8 18 sstrid 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> ( f supp Z ) C_ NN0 )
20 19 ex 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( f e. M -> ( f supp Z ) C_ NN0 ) )
21 7 20 ralrimi 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> A. f e. M ( f supp Z ) C_ NN0 )
22 iunss 
 |-  ( U_ f e. M ( f supp Z ) C_ NN0 <-> A. f e. M ( f supp Z ) C_ NN0 )
23 21 22 sylibr 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> U_ f e. M ( f supp Z ) C_ NN0 )
24 1 23 eqsstrid 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> U C_ NN0 )
25 ltso 
 |-  < Or RR
26 25 a1i 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> < Or RR )
27 simp2 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> M e. Fin )
28 id 
 |-  ( f finSupp Z -> f finSupp Z )
29 28 fsuppimpd 
 |-  ( f finSupp Z -> ( f supp Z ) e. Fin )
30 29 ralimi 
 |-  ( A. f e. M f finSupp Z -> A. f e. M ( f supp Z ) e. Fin )
31 30 adantr 
 |-  ( ( A. f e. M f finSupp Z /\ U =/= (/) ) -> A. f e. M ( f supp Z ) e. Fin )
32 iunfi 
 |-  ( ( M e. Fin /\ A. f e. M ( f supp Z ) e. Fin ) -> U_ f e. M ( f supp Z ) e. Fin )
33 27 31 32 syl2an 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> U_ f e. M ( f supp Z ) e. Fin )
34 1 33 eqeltrid 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> U e. Fin )
35 simprr 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> U =/= (/) )
36 9 10 11 3syl 
 |-  ( ( M C_ ( R ^m NN0 ) /\ f e. M ) -> dom f = NN0 )
37 36 ex 
 |-  ( M C_ ( R ^m NN0 ) -> ( f e. M -> dom f = NN0 ) )
38 37 3ad2ant1 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( f e. M -> dom f = NN0 ) )
39 38 adantr 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( f e. M -> dom f = NN0 ) )
40 39 imp 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> dom f = NN0 )
41 nn0ssre 
 |-  NN0 C_ RR
42 40 41 eqsstrdi 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> dom f C_ RR )
43 8 42 sstrid 
 |-  ( ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) /\ f e. M ) -> ( f supp Z ) C_ RR )
44 43 ex 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> ( f e. M -> ( f supp Z ) C_ RR ) )
45 7 44 ralrimi 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> A. f e. M ( f supp Z ) C_ RR )
46 1 sseq1i 
 |-  ( U C_ RR <-> U_ f e. M ( f supp Z ) C_ RR )
47 iunss 
 |-  ( U_ f e. M ( f supp Z ) C_ RR <-> A. f e. M ( f supp Z ) C_ RR )
48 46 47 bitri 
 |-  ( U C_ RR <-> A. f e. M ( f supp Z ) C_ RR )
49 45 48 sylibr 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> U C_ RR )
50 fisupcl 
 |-  ( ( < Or RR /\ ( U e. Fin /\ U =/= (/) /\ U C_ RR ) ) -> sup ( U , RR , < ) e. U )
51 2 50 eqeltrid 
 |-  ( ( < Or RR /\ ( U e. Fin /\ U =/= (/) /\ U C_ RR ) ) -> S e. U )
52 26 34 35 49 51 syl13anc 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> S e. U )
53 24 52 sseldd 
 |-  ( ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) /\ ( A. f e. M f finSupp Z /\ U =/= (/) ) ) -> S e. NN0 )
54 53 ex 
 |-  ( ( M C_ ( R ^m NN0 ) /\ M e. Fin /\ Z e. V ) -> ( ( A. f e. M f finSupp Z /\ U =/= (/) ) -> S e. NN0 ) )