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 ⊢ 𝐷 = { 𝑓 ∈ ( ℕ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 ≤ 𝐹 ) → 𝐺 ∈ 𝐷 )