Theorem psrbaglecl

Description: The set of finite bags is downward-closed. (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	psrbaglecl	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G e. D )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		simp2	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G : I --> NN0 )
3		simp1	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> F e. D )
4		id	|- ( F e. D -> F e. D )
5	1	psrbagf	|- ( F e. D -> F : I --> NN0 )
6	5	ffnd	|- ( F e. D -> F Fn I )
7	4 6	fndmexd	|- ( F e. D -> I e. _V )
8	7	3ad2ant1	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> I e. _V )
9	1	psrbag	|- ( I e. _V -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
10	8 9	syl	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F e. D <-> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) ) )
11	3 10	mpbid	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( F : I --> NN0 /\ ( `' F " NN ) e. Fin ) )
12	11	simprd	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' F " NN ) e. Fin )
13	1	psrbaglesupp	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' G " NN ) C_ ( `' F " NN ) )
14	12 13	ssfid	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( `' G " NN ) e. Fin )
15	1	psrbag	|- ( I e. _V -> ( G e. D <-> ( G : I --> NN0 /\ ( `' G " NN ) e. Fin ) ) )
16	8 15	syl	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> ( G e. D <-> ( G : I --> NN0 /\ ( `' G " NN ) e. Fin ) ) )
17	2 14 16	mpbir2and	|- ( ( F e. D /\ G : I --> NN0 /\ G oR <_ F ) -> G e. D )