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 ∈ ℕ 0 I | f -1 ℕ ∈ Fin
Assertion psrbaglesuppOLD ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G -1 ℕ ⊆ F -1 ℕ

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ D = f ∈ ℕ 0 I | f -1 ℕ ∈ Fin
2 frnnn0supp ⊢ I ∈ V ∧ G : I ⟶ ℕ 0 → G supp 0 = G -1 ℕ
3 2 3ad2antr2 ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G supp 0 = G -1 ℕ
4 simpr2 ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G : I ⟶ ℕ 0
5 eldifi ⊢ x ∈ I ∖ F -1 ℕ → x ∈ I
6 simpr3 ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G ≤ f F
7 4 ffnd ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G Fn I
8 1 psrbagfOLD ⊢ I ∈ V ∧ F ∈ D → F : I ⟶ ℕ 0
9 8 3ad2antr1 ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F : I ⟶ ℕ 0
10 9 ffnd ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F Fn I
11 simpl ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → I ∈ V
12 inidm ⊢ I ∩ I = I
13 eqidd ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I → G ⁡ x = G ⁡ x
14 eqidd ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I → F ⁡ x = F ⁡ x
15 7 10 11 11 12 13 14 ofrfval ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G ≤ f F ↔ ∀ x ∈ I G ⁡ x ≤ F ⁡ x
16 6 15 mpbid ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → ∀ x ∈ I G ⁡ x ≤ F ⁡ x
17 16 r19.21bi ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I → G ⁡ x ≤ F ⁡ x
18 5 17 sylan2 ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I ∖ F -1 ℕ → G ⁡ x ≤ F ⁡ x
19 11 9 jca ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → I ∈ V ∧ F : I ⟶ ℕ 0
20 frnnn0supp ⊢ I ∈ V ∧ F : I ⟶ ℕ 0 → F supp 0 = F -1 ℕ
21 eqimss ⊢ F supp 0 = F -1 ℕ → F supp 0 ⊆ F -1 ℕ
22 19 20 21 3syl ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → F supp 0 ⊆ F -1 ℕ
23 c0ex ⊢ 0 ∈ V
24 23 a1i ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → 0 ∈ V
25 9 22 11 24 suppssr ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I ∖ F -1 ℕ → F ⁡ x = 0
26 18 25 breqtrd ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I ∖ F -1 ℕ → G ⁡ x ≤ 0
27 ffvelrn ⊢ G : I ⟶ ℕ 0 ∧ x ∈ I → G ⁡ x ∈ ℕ 0
28 4 5 27 syl2an ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I ∖ F -1 ℕ → G ⁡ x ∈ ℕ 0
29 28 nn0ge0d ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ x ∈ I ∖ F -1 ℕ → 0 ≤ G ⁡ x
30 28 nn0red ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F ∧ 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 ≤ f F ∧ 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 ≤ f F ∧ x ∈ I ∖ F -1 ℕ → G ⁡ x = 0
35 4 34 suppss ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G supp 0 ⊆ F -1 ℕ
36 3 35 eqsstrrd ⊢ I ∈ V ∧ F ∈ D ∧ G : I ⟶ ℕ 0 ∧ G ≤ f F → G -1 ℕ ⊆ F -1 ℕ