Metamath Proof Explorer

Theorem psrbagconclOLD

Description: Obsolete version of psrbagconcl as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
psrbagconf1o.s ⊢ S = y ∈ D | y ≤ f F
Assertion psrbagconclOLD ⊢ I ∈ V ∧ 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 simp1 ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → I ∈ V
4 simp2 ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → F ∈ D
5 simp3 ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → X ∈ S
6 breq1 ⊢ y = X → y ≤ f F ↔ X ≤ f F
7 6 2 elrab2 ⊢ X ∈ S ↔ X ∈ D ∧ X ≤ f F
8 5 7 sylib ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → X ∈ D ∧ X ≤ f F
9 8 simpld ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → X ∈ D
10 1 psrbagfOLD ⊢ I ∈ V ∧ X ∈ D → X : I ⟶ ℕ 0
11 3 9 10 syl2anc ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → X : I ⟶ ℕ 0
12 8 simprd ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → X ≤ f F
13 1 psrbagconOLD ⊢ I ∈ V ∧ F ∈ D ∧ X : I ⟶ ℕ 0 ∧ X ≤ f F → F − f X ∈ D ∧ F − f X ≤ f F
14 3 4 11 12 13 syl13anc ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → F − f X ∈ D ∧ F − f X ≤ f F
15 breq1 ⊢ y = F − f X → y ≤ f F ↔ F − f X ≤ f F
16 15 2 elrab2 ⊢ F − f X ∈ S ↔ F − f X ∈ D ∧ F − f X ≤ f F
17 14 16 sylibr ⊢ I ∈ V ∧ F ∈ D ∧ X ∈ S → F − f X ∈ S