This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℕ 0 I | f -1 ℕ ∈ Fin
Assertion psrbaglecl ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G ∈ D

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 simp2 ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G : I ⟶ ℕ 0
3 simp1 ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F ∈ D
4 id ⊢ F ∈ D → F ∈ D
5 1 psrbagf ⊢ F ∈ D → F : I ⟶ ℕ 0
6 5 ffnd ⊢ F ∈ D → F Fn I
7 4 6 fndmexd ⊢ F ∈ D → I ∈ V
8 7 3ad2ant1 ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → I ∈ V
9 1 psrbag ⊢ I ∈ V → F ∈ D ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
10 8 9 syl ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F ∈ D ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
11 3 10 mpbid ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
12 11 simprd ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F -1 ℕ ∈ Fin
13 1 psrbaglesupp ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G -1 ℕ ⊆ F -1 ℕ
14 12 13 ssfid ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G -1 ℕ ∈ Fin
15 1 psrbag ⊢ I ∈ V → G ∈ D ↔ G : I ⟶ ℕ 0 ∧ G -1 ℕ ∈ Fin
16 8 15 syl ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G ∈ D ↔ G : I ⟶ ℕ 0 ∧ G -1 ℕ ∈ Fin
17 2 14 16 mpbir2and ⊢ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G ∈ D