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	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	psrbagconf1o.s	⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
Assertion	psrbagconclOLD	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		psrbagconf1o.s	⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
3		simp1	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐼 ∈ 𝑉 )
4		simp2	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝐹 ∈ 𝐷 )
5		simp3	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
6		breq1	⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹 ) )
7	6 2	elrab2	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
8	5 7	sylib	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
9	8	simpld	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝐷 )
10	1	psrbagfOLD	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐷 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
11	3 9 10	syl2anc	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
12	8	simprd	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∘r ≤ 𝐹 )
13	1	psrbagconOLD	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝑋 : 𝐼 ⟶ ℕ0 ∧ 𝑋 ∘r ≤ 𝐹 ) ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
14	3 4 11 12 13	syl13anc	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
15		breq1	⊢ ( 𝑦 = ( 𝐹 ∘f − 𝑋 ) → ( 𝑦 ∘r ≤ 𝐹 ↔ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
16	15 2	elrab2	⊢ ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 ↔ ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
17	14 16	sylibr	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐹 ∘f − 𝑋 ) ∈ 𝑆 )