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		breq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹 ) )
5	4 2	elrab2	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
6	5	bilani	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
7	6	simpld	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐷 )
8	1	psrbagf	⊢ ( 𝑋 ∈ 𝐷 → 𝑋 : 𝐼 ⟶ ℕ0 )
9	7 8	syl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
10	6	simprd	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∘r ≤ 𝐹 )
11	1	psrbagcon	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 : 𝐼 ⟶ ℕ0 ∧ 𝑋 ∘r ≤ 𝐹 ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
12	3 9 10 11	syl3anc	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
13		breq1	⊢ ( 𝑦 = ( 𝐹 ∘f − 𝑋 ) → ( 𝑦 ∘r ≤ 𝐹 ↔ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
14	13 2	elrab2	⊢ ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 ↔ ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
15	12 14	sylibr	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 )