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 simpr ⊢ F ∈ D ∧ X ∈ S → X ∈ S
5 breq1 ⊢ y = X → y ≤ f F ↔ X ≤ f F
6 5 2 elrab2 ⊢ X ∈ S ↔ X ∈ D ∧ X ≤ f F
7 4 6 sylib ⊢ F ∈ D ∧ X ∈ S → X ∈ D ∧ X ≤ f F
8 7 simpld ⊢ F ∈ D ∧ X ∈ S → X ∈ D
9 1 psrbagf ⊢ X ∈ D → X : I ⟶ ℕ 0
10 8 9 syl ⊢ F ∈ D ∧ X ∈ S → X : I ⟶ ℕ 0
11 7 simprd ⊢ F ∈ D ∧ X ∈ S → X ≤ f F
12 1 psrbagcon ⊢ F ∈ D ∧ X : I ⟶ ℕ 0 ∧ X ≤ f F → F − f X ∈ D ∧ F − f X ≤ f F
13 3 10 11 12 syl3anc ⊢ F ∈ D ∧ X ∈ S → F − f X ∈ D ∧ F − f X ≤ f F
14 breq1 ⊢ y = F − f X → y ≤ f F ↔ F − f X ≤ f F
15 14 2 elrab2 ⊢ F − f X ∈ S ↔ F − f X ∈ D ∧ F − f X ≤ f F
16 13 15 sylibr ⊢ F ∈ D ∧ X ∈ S → F − f X ∈ S