Metamath Proof Explorer

Theorem gsumbagdiaglem

Description: Lemma for gsumbagdiag . (Contributed by Mario Carneiro, 5-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.1 ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
3 gsumbagdiag.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
4 gsumbagdiag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐷 )
5 simprr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } )
6 breq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ↔ 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ) )
7 6 elrab ⊢ ( 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ↔ ( 𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ) )
8 5 7 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ) )
9 8 simpld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∈ 𝐷 )
10 8 simprd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) )
11 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝐼 ∈ 𝑉 )
12 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝐹 ∈ 𝐷 )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∈ 𝑆 )
14 breq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑋 ∘r ≤ 𝐹 ) )
15 14 2 elrab2 ⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
16 13 15 sylib ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑋 ∈ 𝐷 ∧ 𝑋 ∘r ≤ 𝐹 ) )
17 16 simpld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∈ 𝐷 )
18 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐷 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
19 11 17 18 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 : 𝐼 ⟶ ℕ0 )
20 16 simprd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∘r ≤ 𝐹 )
21 1 psrbagcon ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝑋 : 𝐼 ⟶ ℕ0 ∧ 𝑋 ∘r ≤ 𝐹 ) ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
22 11 12 19 20 21 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) )
23 22 simprd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 )
24 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑌 ∈ 𝐷 ) → 𝑌 : 𝐼 ⟶ ℕ0 )
25 11 9 24 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 : 𝐼 ⟶ ℕ0 )
26 22 simpld ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 )
27 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘f − 𝑋 ) ∈ 𝐷 ) → ( 𝐹 ∘f − 𝑋 ) : 𝐼 ⟶ ℕ0 )
28 11 26 27 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) : 𝐼 ⟶ ℕ0 )
29 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
30 11 12 29 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘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 11 25 28 30 36 caoftrn ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( ( 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ∧ ( 𝐹 ∘f − 𝑋 ) ∘r ≤ 𝐹 ) → 𝑌 ∘r ≤ 𝐹 ) )
38 10 23 37 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∘r ≤ 𝐹 )
39 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∘r ≤ 𝐹 ↔ 𝑌 ∘r ≤ 𝐹 ) )
40 39 2 elrab2 ⊢ ( 𝑌 ∈ 𝑆 ↔ ( 𝑌 ∈ 𝐷 ∧ 𝑌 ∘r ≤ 𝐹 ) )
41 9 38 40 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 ∈ 𝑆 )
42 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ↔ 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ) )
43 19 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) ∈ ℕ0 )
44 25 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
45 30 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 25 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑧 ) ) )
57 30 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝐹 Fn 𝐼 )
58 19 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 Fn 𝐼 )
59 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
60 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
61 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑋 ‘ 𝑧 ) = ( 𝑋 ‘ 𝑧 ) )
62 57 58 11 11 59 60 61 offval ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑋 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) )
63 11 44 55 56 62 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑌 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑋 ‘ 𝑧 ) ) ) )
64 ovexd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ∈ V )
65 19 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 = ( 𝑧 ∈ 𝐼 ↦ ( 𝑋 ‘ 𝑧 ) ) )
66 25 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑌 Fn 𝐼 )
67 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) ∧ 𝑧 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) = ( 𝑌 ‘ 𝑧 ) )
68 57 66 11 11 59 60 67 offval ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝐹 ∘f − 𝑌 ) = ( 𝑧 ∈ 𝐼 ↦ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
69 11 43 64 65 68 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ↔ ∀ 𝑧 ∈ 𝐼 ( 𝑋 ‘ 𝑧 ) ≤ ( ( 𝐹 ‘ 𝑧 ) − ( 𝑌 ‘ 𝑧 ) ) ) )
70 54 63 69 3bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) ↔ 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) ) )
71 10 70 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) )
72 42 17 71 elrabd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) } )
73 41 72 jca ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑋 ) } ) ) → ( 𝑌 ∈ 𝑆 ∧ 𝑋 ∈ { 𝑥 ∈ 𝐷 ∣ 𝑥 ∘r ≤ ( 𝐹 ∘f − 𝑌 ) } ) )