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	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion	psrbaglecl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 ∈ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		simp2	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 : 𝐼 ⟶ ℕ0 )
3		simp1	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐹 ∈ 𝐷 )
4		id	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 ∈ 𝐷 )
5	1	psrbagf	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
6	5	ffnd	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼 )
7	4 6	fndmexd	⊢ ( 𝐹 ∈ 𝐷 → 𝐼 ∈ V )
8	7	3ad2ant1	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐼 ∈ V )
9	1	psrbag	⊢ ( 𝐼 ∈ V → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) )
10	8 9	syl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) )
11	3 10	mpbid	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) )
12	11	simprd	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ 𝐹 “ ℕ ) ∈ Fin )
13	1	psrbaglesupp	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ 𝐺 “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )
14	12 13	ssfid	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ 𝐺 “ ℕ ) ∈ Fin )
15	1	psrbag	⊢ ( 𝐼 ∈ V → ( 𝐺 ∈ 𝐷 ↔ ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐺 “ ℕ ) ∈ Fin ) ) )
16	8 15	syl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐺 ∈ 𝐷 ↔ ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐺 “ ℕ ) ∈ Fin ) ) )
17	2 14 16	mpbir2and	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 ∈ 𝐷 )