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

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ 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𝑋 ) ∈ 𝑆 )