Metamath Proof Explorer

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 \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	Assertion	psrbaglecl	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G \in D$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		simp2	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G : I ⟶ ℕ_{0}$
3		simp1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F \in D$
4		id	$⊢ F \in D \to F \in D$
5	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
6	5	ffnd	$⊢ F \in D \to F Fn I$
7	4 6	fndmexd	$⊢ F \in D \to I \in V$
8	7	3ad2ant1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to I \in V$
9	1	psrbag	$⊢ I \in V \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
10	8 9	syl	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
11	3 10	mpbid	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin)$
12	11	simprd	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F^{-1} [ℕ] \in Fin$
13	1	psrbaglesupp	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G^{-1} [ℕ] \subseteq F^{-1} [ℕ]$
14	12 13	ssfid	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G^{-1} [ℕ] \in Fin$
15	1	psrbag	$⊢ I \in V \to (G \in D \leftrightarrow (G : I ⟶ ℕ_{0} \land G^{-1} [ℕ] \in Fin))$
16	8 15	syl	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (G \in D \leftrightarrow (G : I ⟶ ℕ_{0} \land G^{-1} [ℕ] \in Fin))$
17	2 14 16	mpbir2and	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G \in D$