Metamath Proof Explorer


Theorem psrbagleclOLD

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

Ref Expression
Hypothesis psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
Assertion psrbagleclOLD ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐺𝐷 )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 simpr2 ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐺 : 𝐼 ⟶ ℕ0 )
3 simpr1 ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐹𝐷 )
4 1 psrbag ( 𝐼𝑉 → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )
5 4 adantr ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐹𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) ) )
6 3 5 mpbid ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( 𝐹 “ ℕ ) ∈ Fin ) )
7 6 simprd ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐹 “ ℕ ) ∈ Fin )
8 1 psrbaglesuppOLD ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺 “ ℕ ) ⊆ ( 𝐹 “ ℕ ) )
9 7 8 ssfid ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺 “ ℕ ) ∈ Fin )
10 1 psrbag ( 𝐼𝑉 → ( 𝐺𝐷 ↔ ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ ( 𝐺 “ ℕ ) ∈ Fin ) ) )
11 10 adantr ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → ( 𝐺𝐷 ↔ ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ ( 𝐺 “ ℕ ) ∈ Fin ) ) )
12 2 9 11 mpbir2and ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝐺 : 𝐼 ⟶ ℕ0𝐺r𝐹 ) ) → 𝐺𝐷 )