psrbagcon

Description: The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for finite bags. (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	psrbagcon	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	\|- D = { f e. ( NN0 ^m I ) \| ( `' f " NN ) e. Fin }
2	1	psrbagf	\|- ( F e. D -> F : I --> NN0 )
3	2	ffnd	\|- ( F e. D -> F Fn I )
4	3	3ad2ant1	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F Fn I )
5		simp2	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G : I --> NN0 )
6	5	ffnd	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G Fn I )
7		id	\|- ( F e. D -> F e. D )
8	7 3	fndmexd	\|- ( F e. D -> I e. _V )
9	8	3ad2ant1	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> I e. _V )
10		inidm	\|- ( I i^i I ) = I
11	4 6 9 9 10	offn	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) Fn I )
12		eqidd	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( F ` x ) = ( F ` x ) )
13		eqidd	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) = ( G ` x ) )
14	4 6 9 9 10 12 13	ofval	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F oF - G ) ` x ) = ( ( F ` x ) - ( G ` x ) ) )
15		simp3	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G oR <_ F )
16	6 4 9 9 10 13 12	ofrfval	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( G oR <_ F <-> A. x e. I ( G ` x ) <_ ( F ` x ) ) )
17	15 16	mpbid	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> A. x e. I ( G ` x ) <_ ( F ` x ) )
18	17	r19.21bi	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) <_ ( F ` x ) )
19	5	ffvelrnda	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) e. NN0 )
20	2	3ad2ant1	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F : I --> NN0 )
21	20	ffvelrnda	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( F ` x ) e. NN0 )
22		nn0sub	\|- ( ( ( G ` x ) e. NN0 /\ ( F ` x ) e. NN0 ) -> ( ( G ` x ) <_ ( F ` x ) <-> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) )
23	19 21 22	syl2anc	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( G ` x ) <_ ( F ` x ) <-> ( ( F ` x ) - ( G ` x ) ) e. NN0 ) )
24	18 23	mpbid	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) e. NN0 )
25	14 24	eqeltrd	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F oF - G ) ` x ) e. NN0 )
26	25	ralrimiva	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> A. x e. I ( ( F oF - G ) ` x ) e. NN0 )
27		ffnfv	\|- ( ( F oF - G ) : I --> NN0 <-> ( ( F oF - G ) Fn I /\ A. x e. I ( ( F oF - G ) ` x ) e. NN0 ) )
28	11 26 27	sylanbrc	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) : I --> NN0 )
29		simp1	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F e. D )
30	1	psrbag	\|- ( I e. _V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
31	9 30	syl	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
32	29 31	mpbid	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
33	32	simprd	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' F " NN ) e. Fin )
34	19	nn0ge0d	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> 0 <_ ( G ` x ) )
35	21	nn0red	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( F ` x ) e. RR )
36	19	nn0red	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( G ` x ) e. RR )
37	35 36	subge02d	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( 0 <_ ( G ` x ) <-> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
38	34 37	mpbid	\|- ( ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) /\ x e. I ) -> ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) )
39	38	ralrimiva	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) )
40	11 4 9 9 10 14 12	ofrfval	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) oR <_ F <-> A. x e. I ( ( F ` x ) - ( G ` x ) ) <_ ( F ` x ) ) )
41	39 40	mpbird	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) oR <_ F )
42	1	psrbaglesupp	\|- ( ( F e. D /\ ( F oF - G ) : I --> NN0 /\ ( F oF - G ) oR <_ F ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) )
43	29 28 41 42	syl3anc	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' ( F oF - G ) " NN ) C_ ( `' F " NN ) )
44	33 43	ssfid	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' ( F oF - G ) " NN ) e. Fin )
45	1	psrbag	\|- ( I e. _V -> ( ( F oF - G ) e. D <-> ( ( F oF - G ) : I --> NN0 /\ ( `' ( F oF - G ) " NN ) e. Fin ) ) )
46	9 45	syl	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) e. D <-> ( ( F oF - G ) : I --> NN0 /\ ( `' ( F oF - G ) " NN ) e. Fin ) ) )
47	28 44 46	mpbir2and	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F oF - G ) e. D )
48	47 41	jca	\|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( ( F oF - G ) e. D /\ ( F oF - G ) oR <_ F ) )

Metamath Proof Explorer

Theorem psrbagcon

Proof