Metamath Proof Explorer

Theorem psrbaglecl

Description: The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypothesis psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
Assertion psrbaglecl ⊢ I ∈ V ∧ 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 simpr2 ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G : I ⟶ ℕ 0
3 simpr1 ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F ∈ D
4 1 psrbag ⊢ I ∈ V → F ∈ D ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
5 4 adantr ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F ∈ D ↔ F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
6 3 5 mpbid ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F : I ⟶ ℕ 0 ∧ F -1 ℕ ∈ Fin
7 6 simprd ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F -1 ℕ ∈ Fin
8 1 psrbaglesupp ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G -1 ℕ ⊆ F -1 ℕ
9 7 8 ssfid ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G -1 ℕ ∈ Fin
10 1 psrbag ⊢ I ∈ V → G ∈ D ↔ G : I ⟶ ℕ 0 ∧ G -1 ℕ ∈ Fin
11 10 adantr ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G ∈ D ↔ G : I ⟶ ℕ 0 ∧ G -1 ℕ ∈ Fin
12 2 9 11 mpbir2and ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G ∈ D