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 − 𝑋 ) ∈ 𝑆 )