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 ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
psrbagconf1o.s ⊢ S = y ∈ D | y ≤ f F
Assertion psrbagconcl ⊢ F ∈ D ∧ X ∈ S → F − f X ∈ S

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 psrbagconf1o.s ⊢ S = y ∈ D | y ≤ f F
3 simpl ⊢ F ∈ D ∧ X ∈ S → F ∈ D
4 breq1 ⊢ y = X → y ≤ f F ↔ X ≤ f F
5 4 2 elrab2 ⊢ X ∈ S ↔ X ∈ D ∧ X ≤ f F
6 5 bilani ⊢ F ∈ D ∧ X ∈ S → X ∈ D ∧ X ≤ f F
7 6 simpld ⊢ F ∈ D ∧ X ∈ S → X ∈ D
8 1 psrbagf ⊢ X ∈ D → X : I ⟶ ℕ 0
9 7 8 syl ⊢ F ∈ D ∧ X ∈ S → X : I ⟶ ℕ 0
10 6 simprd ⊢ F ∈ D ∧ X ∈ S → X ≤ f F
11 1 psrbagcon ⊢ F ∈ D ∧ X : I ⟶ ℕ 0 ∧ X ≤ f F → F − f X ∈ D ∧ F − f X ≤ f F
12 3 9 10 11 syl3anc ⊢ F ∈ D ∧ X ∈ S → F − f X ∈ D ∧ F − f X ≤ f F
13 breq1 ⊢ y = F − f X → y ≤ f F ↔ F − f X ≤ f F
14 13 2 elrab2 ⊢ F − f X ∈ S ↔ F − f X ∈ D ∧ F − f X ≤ f F
15 12 14 sylibr ⊢ F ∈ D ∧ X ∈ S → F − f X ∈ S