Metamath Proof Explorer

Theorem gsumbagdiaglem

Description: Lemma for gsumbagdiag . (Contributed by Mario Carneiro, 5-Jan-2015) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024)

Ref Expression
Hypotheses gsumbagdiag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
gsumbagdiag.s ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
gsumbagdiag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
Assertion gsumbagdiaglem ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∈ 𝑆 ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) } ) )

Proof

Step Hyp Ref Expression
1 gsumbagdiag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 gsumbagdiag.s ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
3 gsumbagdiag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
4 simprr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } )
5 breq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ↔ 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ) )
6 5 elrab ⊢ ( 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ↔ ( 𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ) )
7 4 6 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ) )
8 7 simpld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∈ 𝐷 )
9 7 simprd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) )
10 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝐹 ∈ 𝐷 )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∈ 𝑆 )
12 breq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹 ) )
13 12 2 elrab2 ⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
14 11 13 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
15 14 simpld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∈ 𝐷 )
16 1 psrbagf ⊢ ( 𝑋 ∈ 𝐷 → 𝑋 : 𝐼 ⟶ ℕ0 )
17 15 16 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 : 𝐼 ⟶ ℕ0 )
18 14 simprd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∘r ≤ 𝐹 )
19 1 psrbagcon ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑋 : 𝐼 ⟶ ℕ0 ∧ 𝑋 ∘r ≤ 𝐹 ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
20 10 17 18 19 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
21 20 simprd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 )
22 1 psrbagf ⊢ ( 𝐹 ∈ 𝐷 → 𝐹 : 𝐼 ⟶ ℕ0 )
23 10 22 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝐹 : 𝐼 ⟶ ℕ0 )
24 23 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝐹 Fn 𝐼 )
25 10 24 fndmexd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝐼 ∈ V )
26 1 psrbagf ⊢ ( 𝑌 ∈ 𝐷 → 𝑌 : 𝐼 ⟶ ℕ0 )
27 8 26 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 : 𝐼 ⟶ ℕ0 )
28 20 simpld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 )
29 1 psrbagf ⊢ ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 → ( 𝐹 ∘f − 𝑋 ) : 𝐼 ⟶ ℕ0 )
30 28 29 syl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) : 𝐼 ⟶ ℕ0 )
31 nn0re ⊢ ( 𝑢 ∈ ℕ0 → 𝑢 ∈ ℝ )
32 nn0re ⊢ ( 𝑣 ∈ ℕ0 → 𝑣 ∈ ℝ )
33 nn0re ⊢ ( 𝑤 ∈ ℕ0 → 𝑤 ∈ ℝ )
34 letr ⊢ ( ( 𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ( ( 𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤 ) → 𝑢 ≤ 𝑤 ) )
35 31 32 33 34 syl3an ⊢ ( ( 𝑢 ∈ ℕ0 ∧ 𝑣 ∈ ℕ0 ∧ 𝑤 ∈ ℕ0 ) → ( ( 𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤 ) → 𝑢 ≤ 𝑤 ) )
36 35 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ ( 𝑢 ∈ ℕ0 ∧ 𝑣 ∈ ℕ0 ∧ 𝑤 ∈ ℕ0 ) ) → ( ( 𝑢 ≤ 𝑣 ∧ 𝑣 ≤ 𝑤 ) → 𝑢 ≤ 𝑤 ) )
37 25 27 30 23 36 caoftrn ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( ( 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) → 𝑌 ∘r ≤ 𝐹 ) )
38 9 21 37 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∘r ≤ 𝐹 )
39 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑌 ∘r ≤ 𝐹 ) )
40 39 2 elrab2 ⊢ ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ 𝐹 ) )
41 8 38 40 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∈ 𝑆 )
42 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ↔ 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ) )
43 17 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 )
44 27 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
45 23 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℕ0 )
46 nn0re ⊢ ( ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑋 ‘ 𝑧 ) ∈ ℝ )
47 nn0re ⊢ ( ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 → ( 𝑌 ‘ 𝑧 ) ∈ ℝ )
48 nn0re ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ℕ0 → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
49 leaddsub2 ⊢ ( ( ( 𝑋 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ≤ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑌 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) )
50 leaddsub ⊢ ( ( ( 𝑋 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( 𝑋 ‘ 𝑧 ) + ( 𝑌 ‘ 𝑧 ) ) ≤ ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
51 49 50 bitr3d ⊢ ( ( ( 𝑋 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( 𝑌 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ↔ ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
52 46 47 48 51 syl3an ⊢ ( ( ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℕ0 ) → ( ( 𝑌 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ↔ ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
53 43 44 45 52 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝑌 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ↔ ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
54 53 ralbidva ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( ∀ 𝑧 ∈ 𝐼 ( 𝑌 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
55 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ∈ V )
56 27 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) )
57 17 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 Fn 𝐼 )
58 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
59 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
60 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) = ( 𝑋 ‘ 𝑧 ) )
61 24 57 25 25 58 59 60 offval ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) )
62 25 44 55 56 61 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑌 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) )
63 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ∈ V )
64 17 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑧 ) ) )
65 27 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 Fn 𝐼 )
66 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) = ( 𝑌 ‘ 𝑧 ) )
67 24 65 25 25 58 59 66 offval ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑌 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
68 25 43 63 64 67 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
69 54 62 68 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ↔ 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ) )
70 9 69 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) )
71 42 15 70 elrabd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) } )
72 41 71 jca ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∈ 𝑆 ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) } ) )