Theorem gsumbagdiaglemOLD 21482

Description: Obsolete version of gsumbagdiaglem 21485 as of 6-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

Ref	Expression
psrbag.d	⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
psrbagconf1o.s	⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹}
gsumbagdiagOLD.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
gsumbagdiagOLD.f	⊢ (𝜑 → 𝐹 ∈ 𝐷)

Assertion

Ref	Expression
gsumbagdiaglemOLD	⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑌 ∈ 𝑆 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑌)}))

Distinct variable groups:   𝑥,𝑓,𝑦,𝐹   𝑥,𝑉,𝑦   𝑓,𝐼,𝑥,𝑦   𝑥,𝑆   𝑥,𝐷,𝑦   𝑓,𝑋,𝑥,𝑦   𝑓,𝑌,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓)   𝐷(𝑓)   𝑆(𝑦,𝑓)   𝑉(𝑓)

Proof of Theorem gsumbagdiaglemOLD

Dummy variables 𝑢 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprr 771	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})
2		breq1 5150	. . . . . 6 ⊢ (𝑥 = 𝑌 → (𝑥 ∘r ≤ (𝐹 ∘f − 𝑋) ↔ 𝑌 ∘r ≤ (𝐹 ∘f − 𝑋)))
3	2	elrab 3682	. . . . 5 ⊢ (𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)} ↔ (𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ (𝐹 ∘f − 𝑋)))
4	1, 3	sylib 217	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ (𝐹 ∘f − 𝑋)))
5	4	simpld 495	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌 ∈ 𝐷)
6	4	simprd 496	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌 ∘r ≤ (𝐹 ∘f − 𝑋))
7		gsumbagdiagOLD.i	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
8	7	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝐼 ∈ 𝑉)
9		gsumbagdiagOLD.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
10	9	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝐹 ∈ 𝐷)
11		simprl 769	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋 ∈ 𝑆)
12		breq1 5150	. . . . . . . . . 10 ⊢ (𝑦 = 𝑋 → (𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹))
13		psrbagconf1o.s	. . . . . . . . . 10 ⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹}
14	12, 13	elrab2 3685	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑆 ↔ (𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹))
15	11, 14	sylib 217	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹))
16	15	simpld 495	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋 ∈ 𝐷)
17		psrbag.d	. . . . . . . 8 ⊢ 𝐷 = {𝑓 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑓 “ ℕ) ∈ Fin}
18	17	psrbagfOLD 21463	. . . . . . 7 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐷) → 𝑋:𝐼⟶ℕ0)
19	8, 16, 18	syl2anc 584	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋:𝐼⟶ℕ0)
20	15	simprd 496	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋 ∘r ≤ 𝐹)
21	17	psrbagconOLD 21475	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝑋:𝐼⟶ℕ0 ∧ 𝑋 ∘r ≤ 𝐹)) → ((𝐹 ∘f − 𝑋) ∈ 𝐷 ∧ (𝐹 ∘f − 𝑋) ∘r ≤ 𝐹))
22	8, 10, 19, 20, 21	syl13anc 1372	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → ((𝐹 ∘f − 𝑋) ∈ 𝐷 ∧ (𝐹 ∘f − 𝑋) ∘r ≤ 𝐹))
23	22	simprd 496	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝐹 ∘f − 𝑋) ∘r ≤ 𝐹)
24	17	psrbagfOLD 21463	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷) → 𝑌:𝐼⟶ℕ0)
25	8, 5, 24	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌:𝐼⟶ℕ0)
26	22	simpld 495	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝐹 ∘f − 𝑋) ∈ 𝐷)
27	17	psrbagfOLD 21463	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘f − 𝑋) ∈ 𝐷) → (𝐹 ∘f − 𝑋):𝐼⟶ℕ0)
28	8, 26, 27	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝐹 ∘f − 𝑋):𝐼⟶ℕ0)
29	17	psrbagfOLD 21463	. . . . . 6 ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0)
30	8, 10, 29	syl2anc 584	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝐹:𝐼⟶ℕ0)
31		nn0re 12477	. . . . . . 7 ⊢ (𝑢 ∈ ℕ0 → 𝑢 ∈ ℝ)
32		nn0re 12477	. . . . . . 7 ⊢ (𝑣 ∈ ℕ0 → 𝑣 ∈ ℝ)
33		nn0re 12477	. . . . . . 7 ⊢ (𝑤 ∈ ℕ0 → 𝑤 ∈ ℝ)
34		letr 11304	. . . . . . 7 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤))
35	31, 32, 33, 34	syl3an 1160	. . . . . 6 ⊢ ((𝑢 ∈ ℕ0 ∧ 𝑣 ∈ ℕ0 ∧ 𝑤 ∈ ℕ0) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤))
36	35	adantl 482	. . . . 5 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ (𝑢 ∈ ℕ0 ∧ 𝑣 ∈ ℕ0 ∧ 𝑤 ∈ ℕ0)) → ((𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤) → 𝑢 ≤ 𝑤))
37	8, 25, 28, 30, 36	caoftrn 7704	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → ((𝑌 ∘r ≤ (𝐹 ∘f − 𝑋) ∧ (𝐹 ∘f − 𝑋) ∘r ≤ 𝐹) → 𝑌 ∘r ≤ 𝐹))
38	6, 23, 37	mp2and 697	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌 ∘r ≤ 𝐹)
39		breq1 5150	. . . 4 ⊢ (𝑦 = 𝑌 → (𝑦 ∘r ≤ 𝐹 ↔ 𝑌 ∘r ≤ 𝐹))
40	39, 13	elrab2 3685	. . 3 ⊢ (𝑌 ∈ 𝑆 ↔ (𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ 𝐹))
41	5, 38, 40	sylanbrc 583	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌 ∈ 𝑆)
42		breq1 5150	. . 3 ⊢ (𝑥 = 𝑋 → (𝑥 ∘r ≤ (𝐹 ∘f − 𝑌) ↔ 𝑋 ∘r ≤ (𝐹 ∘f − 𝑌)))
43	19	ffvelcdmda 7083	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) ∈ ℕ0)
44	25	ffvelcdmda 7083	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) ∈ ℕ0)
45	30	ffvelcdmda 7083	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ ℕ0)
46		nn0re 12477	. . . . . . . 8 ⊢ ((𝑋‘𝑧) ∈ ℕ0 → (𝑋‘𝑧) ∈ ℝ)
47		nn0re 12477	. . . . . . . 8 ⊢ ((𝑌‘𝑧) ∈ ℕ0 → (𝑌‘𝑧) ∈ ℝ)
48		nn0re 12477	. . . . . . . 8 ⊢ ((𝐹‘𝑧) ∈ ℕ0 → (𝐹‘𝑧) ∈ ℝ)
49		leaddsub2 11687	. . . . . . . . 9 ⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝑋‘𝑧) + (𝑌‘𝑧)) ≤ (𝐹‘𝑧) ↔ (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧))))
50		leaddsub 11686	. . . . . . . . 9 ⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → (((𝑋‘𝑧) + (𝑌‘𝑧)) ≤ (𝐹‘𝑧) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧))))
51	49, 50	bitr3d 280	. . . . . . . 8 ⊢ (((𝑋‘𝑧) ∈ ℝ ∧ (𝑌‘𝑧) ∈ ℝ ∧ (𝐹‘𝑧) ∈ ℝ) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧))))
52	46, 47, 48, 51	syl3an 1160	. . . . . . 7 ⊢ (((𝑋‘𝑧) ∈ ℕ0 ∧ (𝑌‘𝑧) ∈ ℕ0 ∧ (𝐹‘𝑧) ∈ ℕ0) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧))))
53	43, 44, 45, 52	syl3anc 1371	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧))))
54	53	ralbidva 3175	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (∀𝑧 ∈ 𝐼 (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧)) ↔ ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧))))
55		ovexd 7440	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑋‘𝑧)) ∈ V)
56	25	feqmptd 6957	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌 = (𝑧 ∈ 𝐼 ↦ (𝑌‘𝑧)))
57	30	ffnd 6715	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝐹 Fn 𝐼)
58	19	ffnd 6715	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋 Fn 𝐼)
59		inidm 4217	. . . . . . 7 ⊢ (𝐼 ∩ 𝐼) = 𝐼
60		eqidd 2733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) = (𝐹‘𝑧))
61		eqidd 2733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑋‘𝑧) = (𝑋‘𝑧))
62	57, 58, 8, 8, 59, 60, 61	offval 7675	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝐹 ∘f − 𝑋) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑋‘𝑧))))
63	8, 44, 55, 56, 62	ofrfval2 7687	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑌 ∘r ≤ (𝐹 ∘f − 𝑋) ↔ ∀𝑧 ∈ 𝐼 (𝑌‘𝑧) ≤ ((𝐹‘𝑧) − (𝑋‘𝑧))))
64		ovexd 7440	. . . . . 6 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑧) − (𝑌‘𝑧)) ∈ V)
65	19	feqmptd 6957	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋 = (𝑧 ∈ 𝐼 ↦ (𝑋‘𝑧)))
66	25	ffnd 6715	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑌 Fn 𝐼)
67		eqidd 2733	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) ∧ 𝑧 ∈ 𝐼) → (𝑌‘𝑧) = (𝑌‘𝑧))
68	57, 66, 8, 8, 59, 60, 67	offval 7675	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝐹 ∘f − 𝑌) = (𝑧 ∈ 𝐼 ↦ ((𝐹‘𝑧) − (𝑌‘𝑧))))
69	8, 43, 64, 65, 68	ofrfval2 7687	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑋 ∘r ≤ (𝐹 ∘f − 𝑌) ↔ ∀𝑧 ∈ 𝐼 (𝑋‘𝑧) ≤ ((𝐹‘𝑧) − (𝑌‘𝑧))))
70	54, 63, 69	3bitr4d 310	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑌 ∘r ≤ (𝐹 ∘f − 𝑋) ↔ 𝑋 ∘r ≤ (𝐹 ∘f − 𝑌)))
71	6, 70	mpbid 231	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋 ∘r ≤ (𝐹 ∘f − 𝑌))
72	42, 16, 71	elrabd 3684	. 2 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑌)})
73	41, 72	jca 512	1 ⊢ ((𝜑 ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑋)})) → (𝑌 ∈ 𝑆 ∧ 𝑋 ∈ {𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ (𝐹 ∘f − 𝑌)}))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3061  {crab 3432  Vcvv 3474   class class class wbr 5147  ^◡ccnv 5674   “ cima 5678  ⟶wf 6536  ‘cfv 6540  (class class class)co 7405   ∘_f cof 7664   ∘_r cofr 7665   ↑_m cmap 8816  Fincfn 8935  ℝcr 11105   + caddc 11109   ≤ cle 11245   − cmin 11440  ℕcn 12208  ℕ₀cn0 12468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-ofr 7667  df-om 7852  df-2nd 7972  df-supp 8143  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-map 8818  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209  df-n0 12469

This theorem is referenced by:  gsumbagdiagOLD  21483  psrass1lemOLD  21484