Metamath Proof Explorer

Theorem psrbaglesuppOLD

Description: Obsolete version of psrbaglesupp as of 5-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
Assertion psrbaglesuppOLD 
|- ( ( I e. V /\ ( 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 frnnn0supp 
 |-  ( ( I e. V /\ G : I --> NN0 ) -> ( G supp 0 ) = ( `' G " NN ) )
3 2 3ad2antr2 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( G supp 0 ) = ( `' G " NN ) )
4 simpr2 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G : I --> NN0 )
5 eldifi 
 |-  ( x e. ( I \ ( `' F " NN ) ) -> x e. I )
6 simpr3 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G oR <_ F )
7 4 ffnd 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> G Fn I )
8 1 psrbagfOLD 
 |-  ( ( I e. V /\ F e. D ) -> F : I --> NN0 )
9 8 3ad2antr1 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F : I --> NN0 )
10 9 ffnd 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> F Fn I )
11 simpl 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> I e. V )
12 inidm 
 |-  ( I i^i I ) = I
13 eqidd 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
14 eqidd 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
15 7 10 11 11 12 13 14 ofrfval 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( G oR <_ F <-> A. x e. I ( G ` x ) <_ ( F ` x ) ) )
16 6 15 mpbid 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> A. x e. I ( G ` x ) <_ ( F ` x ) )
17 16 r19.21bi 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. I ) -> ( G ` x ) <_ ( F ` x ) )
18 5 17 sylan2 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) <_ ( F ` x ) )
19 11 9 jca 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( I e. V /\ F : I --> NN0 ) )
20 frnnn0supp 
 |-  ( ( I e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )
21 eqimss 
 |-  ( ( F supp 0 ) = ( `' F " NN ) -> ( F supp 0 ) C_ ( `' F " NN ) )
22 19 20 21 3syl 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( F supp 0 ) C_ ( `' F " NN ) )
23 c0ex 
 |-  0 e. _V
24 23 a1i 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> 0 e. _V )
25 9 22 11 24 suppssr 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( F ` x ) = 0 )
26 18 25 breqtrd 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) <_ 0 )
27 ffvelrn 
 |-  ( ( G : I --> NN0 /\ x e. I ) -> ( G ` x ) e. NN0 )
28 4 5 27 syl2an 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) e. NN0 )
29 28 nn0ge0d 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> 0 <_ ( G ` x ) )
30 28 nn0red 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) e. RR )
31 0re 
 |-  0 e. RR
32 letri3 
 |-  ( ( ( G ` x ) e. RR /\ 0 e. RR ) -> ( ( G ` x ) = 0 <-> ( ( G ` x ) <_ 0 /\ 0 <_ ( G ` x ) ) ) )
33 30 31 32 sylancl 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( ( G ` x ) = 0 <-> ( ( G ` x ) <_ 0 /\ 0 <_ ( G ` x ) ) ) )
34 26 29 33 mpbir2and 
 |-  ( ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) /\ x e. ( I \ ( `' F " NN ) ) ) -> ( G ` x ) = 0 )
35 4 34 suppss 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( G supp 0 ) C_ ( `' F " NN ) )
36 3 35 eqsstrrd 
 |-  ( ( I e. V /\ ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) ) -> ( `' G " NN ) C_ ( `' F " NN ) )