Theorem psrbaglesupp

Description: The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

	Ref	Expression
Hypothesis	psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
Assertion	psrbaglesupp	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ 𝐺 “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		df-ofr	⊢ ∘r ≤ = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∀ 𝑐 ∈ ( dom 𝑎 ∩ dom 𝑏 ) ( 𝑎 ‘ 𝑐 ) ≤ ( 𝑏 ‘ 𝑐 ) }
3	2	relopabiv	⊢ Rel ∘r ≤
4	3	brrelex1i	⊢ ( 𝐺 ∘r ≤ 𝐹 → 𝐺 ∈ V )
5	4	3ad2ant3	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 ∈ V )
6		simp2	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 : 𝐼 ⟶ ℕ0 )
7		fcdmnn0suppg	⊢ ( ( 𝐺 ∈ V ∧ 𝐺 : 𝐼 ⟶ ℕ0 ) → ( 𝐺 supp 0 ) = ( ◡ 𝐺 “ ℕ ) )
8	5 6 7	syl2anc	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐺 supp 0 ) = ( ◡ 𝐺 “ ℕ ) )
9		eldifi	⊢ ( 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) → 𝑥 ∈ 𝐼 )
10		simp3	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 ∘r ≤ 𝐹 )
11	6	ffnd	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐺 Fn 𝐼 )
12	1	psrbagf	⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
13	12	3ad2ant1	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
14	13	ffnd	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐹 Fn 𝐼 )
15		simp1	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 𝐹 ∈ 𝐷 )
16		inidm	⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
17		eqidd	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
18		eqidd	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19	11 14 5 15 16 17 18	ofrfvalg	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐺 ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
20	10 19	mpbid	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ∀ 𝑥 ∈ 𝐼 ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
21	20	r19.21bi	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
22	9 21	sylan2	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
23		fcdmnn0suppg	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐹 : 𝐼 ⟶ ℕ0 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) )
24	15 13 23	syl2anc	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) )
25		eqimss	⊢ ( ( 𝐹 supp 0 ) = ( ◡ 𝐹 “ ℕ ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ℕ ) )
26	24 25	syl	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐹 supp 0 ) ⊆ ( ◡ 𝐹 “ ℕ ) )
27		c0ex	⊢ 0 ∈ V
28	27	a1i	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → 0 ∈ V )
29	13 26 15 28	suppssrg	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
30	22 29	breqtrd	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑥 ) ≤ 0 )
31		ffvelcdm	⊢ ( ( 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 )
32	6 9 31	syl2an	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℕ0 )
33	32	nn0ge0d	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → 0 ≤ ( 𝐺 ‘ 𝑥 ) )
34	32	nn0red	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
35		0re	⊢ 0 ∈ ℝ
36		letri3	⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( 𝐺 ‘ 𝑥 ) = 0 ↔ ( ( 𝐺 ‘ 𝑥 ) ≤ 0 ∧ 0 ≤ ( 𝐺 ‘ 𝑥 ) ) ) )
37	34 35 36	sylancl	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( ( 𝐺 ‘ 𝑥 ) = 0 ↔ ( ( 𝐺 ‘ 𝑥 ) ≤ 0 ∧ 0 ≤ ( 𝐺 ‘ 𝑥 ) ) ) )
38	30 33 37	mpbir2and	⊢ ( ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) ∧ 𝑥 ∈ ( 𝐼 ∖ ( ◡ 𝐹 “ ℕ ) ) ) → ( 𝐺 ‘ 𝑥 ) = 0 )
39	6 38	suppss	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( 𝐺 supp 0 ) ⊆ ( ◡ 𝐹 “ ℕ ) )
40	8 39	eqsstrrd	⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝐺 : 𝐼 ⟶ ℕ0 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ◡ 𝐺 “ ℕ ) ⊆ ( ◡ 𝐹 “ ℕ ) )