Metamath Proof Explorer

Theorem psrbaglesuppOLD

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

Ref Expression
Hypothesis psrbag.d ⊢D=f∈ℕ0I|f-1ℕ∈Fin
Assertion psrbaglesuppOLD ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→G-1ℕ⊆F-1ℕ

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢D=f∈ℕ0I|f-1ℕ∈Fin
2 fcdmnn0supp ⊢I∈V∧G:I⟶ℕ0→Gsupp0=G-1ℕ
3 2 3ad2antr2 ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→Gsupp0=G-1ℕ
4 simpr2 ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→G:I⟶ℕ0
5 eldifi ⊢x∈I∖F-1ℕ→x∈I
6 simpr3 ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→G≤fF
7 4 ffnd ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→GFnI
8 1 psrbagfOLD ⊢I∈V∧F∈D→F:I⟶ℕ0
9 8 3ad2antr1 ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→F:I⟶ℕ0
10 9 ffnd ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→FFnI
11 simpl ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→I∈V
12 inidm ⊢I∩I=I
13 eqidd ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I→G⁡x=G⁡x
14 eqidd ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I→F⁡x=F⁡x
15 7 10 11 11 12 13 14 ofrfval ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→G≤fF↔∀x∈IG⁡x≤F⁡x
16 6 15 mpbid ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→∀x∈IG⁡x≤F⁡x
17 16 r19.21bi ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I→G⁡x≤F⁡x
18 5 17 sylan2 ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→G⁡x≤F⁡x
19 11 9 jca ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→I∈V∧F:I⟶ℕ0
20 fcdmnn0supp ⊢I∈V∧F:I⟶ℕ0→Fsupp0=F-1ℕ
21 eqimss ⊢Fsupp0=F-1ℕ→Fsupp0⊆F-1ℕ
22 19 20 21 3syl ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→Fsupp0⊆F-1ℕ
23 c0ex ⊢0∈V
24 23 a1i ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→0∈V
25 9 22 11 24 suppssr ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→F⁡x=0
26 18 25 breqtrd ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→G⁡x≤0
27 ffvelcdm ⊢G:I⟶ℕ0∧x∈I→G⁡x∈ℕ0
28 4 5 27 syl2an ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→G⁡x∈ℕ0
29 28 nn0ge0d ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→0≤G⁡x
30 28 nn0red ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→G⁡x∈ℝ
31 0re ⊢0∈ℝ
32 letri3 ⊢G⁡x∈ℝ∧0∈ℝ→G⁡x=0↔G⁡x≤0∧0≤G⁡x
33 30 31 32 sylancl ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→G⁡x=0↔G⁡x≤0∧0≤G⁡x
34 26 29 33 mpbir2and ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF∧x∈I∖F-1ℕ→G⁡x=0
35 4 34 suppss ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→Gsupp0⊆F-1ℕ
36 3 35 eqsstrrd ⊢I∈V∧F∈D∧G:I⟶ℕ0∧G≤fF→G-1ℕ⊆F-1ℕ