Metamath Proof Explorer

Theorem psrbaglesupp

Description: The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

Ref Expression
Hypothesis psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbaglesupp 
|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' G " NN ) C_ ( `' F " NN ) )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 df-ofr 
 |-  oR <_ = { <. a , b >. | A. c e. ( dom a i^i dom b ) ( a ` c ) <_ ( b ` c ) }
3 2 relopabiv 
 |-  Rel oR <_
4 3 brrelex1i 
 |-  ( G oR <_ F -> G e. _V )
5 4 3ad2ant3 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G e. _V )
6 simp2 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G : I --> NN0 )
7 frnnn0suppg 
 |-  ( ( G e. _V /\ G : I --> NN0 ) -> ( G supp 0 ) = ( `' G " NN ) )
8 5 6 7 syl2anc 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( G supp 0 ) = ( `' G " NN ) )
9 eldifi 
 |-  ( x e. ( I \ ( `' F " NN ) ) -> x e. I )
10 simp3 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G oR <_ F )
11 6 ffnd 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G Fn I )
12 1 psrbagf 
 |-  ( F e. D -> F : I --> NN0 )
13 12 3ad2ant1 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F : I --> NN0 )
14 13 ffnd 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F Fn I )
15 simp1 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F e. D )
16 inidm 
 |-  ( I i^i I ) = I
17 eqidd 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
18 eqidd 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
19 11 14 5 15 16 17 18 ofrfvalg 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( G oR <_ F <-> A. x e. I ( G ` x ) <_ ( F ` x ) ) )
20 10 19 mpbid 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> A. x e. I ( G ` x ) <_ ( F ` x ) )
21 20 r19.21bi 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) <_ ( F ` x ) )
22 9 21 sylan2 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) <_ ( F ` x ) )
23 frnnn0suppg 
 |-  ( ( F e. D /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )
24 15 13 23 syl2anc 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F supp 0 ) = ( `' F " NN ) )
25 eqimss 
 |-  ( ( F supp 0 ) = ( `' F " NN ) -> ( F supp 0 ) C_ ( `' F " NN ) )
26 24 25 syl 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F supp 0 ) C_ ( `' F " NN ) )
27 c0ex 
 |-  0 e. _V
28 27 a1i 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> 0 e. _V )
29 13 26 15 28 suppssrg 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( F ` x ) = 0 )
30 22 29 breqtrd 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) <_ 0 )
31 ffvelrn 
 |-  ( ( G : I --> NN0 /\ x e. I ) -> ( G ` x ) e. NN0 )
32 6 9 31 syl2an 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) e. NN0 )
33 32 nn0ge0d 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> 0 <_ ( G ` x ) )
34 32 nn0red 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) e. RR )
35 0re 
 |-  0 e. RR
36 letri3 
 |-  ( ( ( G ` x ) e. RR /\ 0 e. RR ) -> ( ( G ` x ) = 0 <-> ( ( G ` x ) <_ 0 /\ 0 <_ ( G ` x ) ) ) )
37 34 35 36 sylancl 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( ( G ` x ) = 0 <-> ( ( G ` x ) <_ 0 /\ 0 <_ ( G ` x ) ) ) )
38 30 33 37 mpbir2and 
 |-  ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) = 0 )
39 6 38 suppss 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( G supp 0 ) C_ ( `' F " NN ) )
40 8 39 eqsstrrd 
 |-  ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' G " NN ) C_ ( `' F " NN ) )