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

Metamath Proof Explorer

Theorem psrbagconcl

Description: The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024)

Ref Expression
Hypotheses psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psrbagconf1o.s ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
Assertion psrbagconcl ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.s ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
3 simpl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐹 ∈ 𝐷 )
4 simpr ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
5 breq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹 ) )
6 5 2 elrab2 ⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
7 4 6 sylib ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
8 7 simpld ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐷 )
9 1 psrbagf ⊢ ( 𝑋 ∈ 𝐷 → 𝑋 : 𝐼 ⟶ ℕ0 )
10 8 9 syl ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
11 7 simprd ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∘r ≤ 𝐹 )
12 1 psrbagcon ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 : 𝐼 ⟶ ℕ0 ∧ 𝑋 ∘r ≤ 𝐹 ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
13 3 10 11 12 syl3anc ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
14 breq1 ⊢ ( 𝑦 = ( 𝐹 ∘f − 𝑋 ) → ( 𝑦 ∘r ≤ 𝐹 ↔ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
15 14 2 elrab2 ⊢ ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 ↔ ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
16 13 15 sylibr ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 )