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	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	gsumbagdiag.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
	gsumbagdiag.f	$⊢ φ \to F \in D$
Assertion	gsumbagdiaglem	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \in S \land X \in \{x \in D \| x \leq_{f} (F -_{f} Y)\})$

Proof

Step	Hyp	Ref	Expression
1		gsumbagdiag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		gsumbagdiag.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		gsumbagdiag.f	$⊢ φ \to F \in D$
4		simprr	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\}$
5		breq1	$⊢ x = Y \to (x \leq_{f} (F -_{f} X) \leftrightarrow Y \leq_{f} (F -_{f} X))$
6	5	elrab	$⊢ Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\} \leftrightarrow (Y \in D \land Y \leq_{f} (F -_{f} X))$
7	4 6	sylib	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \in D \land Y \leq_{f} (F -_{f} X))$
8	7	simpld	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \in D$
9	7	simprd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \leq_{f} (F -_{f} X)$
10	3	adantr	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F \in D$
11		simprl	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \in S$
12		breq1	$⊢ y = X \to (y \leq_{f} F \leftrightarrow X \leq_{f} F)$
13	12 2	elrab2	$⊢ X \in S \leftrightarrow (X \in D \land X \leq_{f} F)$
14	11 13	sylib	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (X \in D \land X \leq_{f} F)$
15	14	simpld	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \in D$
16	1	psrbagf	$⊢ X \in D \to X : I ⟶ ℕ_{0}$
17	15 16	syl	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X : I ⟶ ℕ_{0}$
18	14	simprd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \leq_{f} F$
19	1	psrbagcon	$⊢ (F \in D \land X : I ⟶ ℕ_{0} \land X \leq_{f} F) \to (F -_{f} X \in D \land (F -_{f} X) \leq_{f} F)$
20	10 17 18 19	syl3anc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (F -_{f} X \in D \land (F -_{f} X) \leq_{f} F)$
21	20	simprd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (F -_{f} X) \leq_{f} F$
22	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
23	10 22	syl	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F : I ⟶ ℕ_{0}$
24	23	ffnd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F Fn I$
25	10 24	fndmexd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to I \in V$
26	1	psrbagf	$⊢ Y \in D \to Y : I ⟶ ℕ_{0}$
27	8 26	syl	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y : I ⟶ ℕ_{0}$
28	20	simpld	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F -_{f} X \in D$
29	1	psrbagf	$⊢ F -_{f} X \in D \to (F -_{f} X) : I ⟶ ℕ_{0}$
30	28 29	syl	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (F -_{f} X) : I ⟶ ℕ_{0}$
31		nn0re	$⊢ u \in ℕ_{0} \to u \in ℝ$
32		nn0re	$⊢ v \in ℕ_{0} \to v \in ℝ$
33		nn0re	$⊢ w \in ℕ_{0} \to w \in ℝ$
34		letr	$⊢ (u \in ℝ \land v \in ℝ \land w \in ℝ) \to ((u \leq v \land v \leq w) \to u \leq w)$
35	31 32 33 34	syl3an	$⊢ (u \in ℕ_{0} \land v \in ℕ_{0} \land w \in ℕ_{0}) \to ((u \leq v \land v \leq w) \to u \leq w)$
36	35	adantl	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land (u \in ℕ_{0} \land v \in ℕ_{0} \land w \in ℕ_{0})) \to ((u \leq v \land v \leq w) \to u \leq w)$
37	25 27 30 23 36	caoftrn	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to ((Y \leq_{f} (F -_{f} X) \land (F -_{f} X) \leq_{f} F) \to Y \leq_{f} F)$
38	9 21 37	mp2and	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \leq_{f} F$
39		breq1	$⊢ y = Y \to (y \leq_{f} F \leftrightarrow Y \leq_{f} F)$
40	39 2	elrab2	$⊢ Y \in S \leftrightarrow (Y \in D \land Y \leq_{f} F)$
41	8 38 40	sylanbrc	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y \in S$
42		breq1	$⊢ x = X \to (x \leq_{f} (F -_{f} Y) \leftrightarrow X \leq_{f} (F -_{f} Y))$
43	17	ffvelcdmda	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to X (z) \in ℕ_{0}$
44	27	ffvelcdmda	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to Y (z) \in ℕ_{0}$
45	23	ffvelcdmda	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) \in ℕ_{0}$
46		nn0re	$⊢ X (z) \in ℕ_{0} \to X (z) \in ℝ$
47		nn0re	$⊢ Y (z) \in ℕ_{0} \to Y (z) \in ℝ$
48		nn0re	$⊢ F (z) \in ℕ_{0} \to F (z) \in ℝ$
49		leaddsub2	$⊢ (X (z) \in ℝ \land Y (z) \in ℝ \land F (z) \in ℝ) \to (X (z) + Y (z) \leq F (z) \leftrightarrow Y (z) \leq F (z) - X (z))$
50		leaddsub	$⊢ (X (z) \in ℝ \land Y (z) \in ℝ \land F (z) \in ℝ) \to (X (z) + Y (z) \leq F (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
51	49 50	bitr3d	$⊢ (X (z) \in ℝ \land Y (z) \in ℝ \land F (z) \in ℝ) \to (Y (z) \leq F (z) - X (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
52	46 47 48 51	syl3an	$⊢ (X (z) \in ℕ_{0} \land Y (z) \in ℕ_{0} \land F (z) \in ℕ_{0}) \to (Y (z) \leq F (z) - X (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
53	43 44 45 52	syl3anc	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to (Y (z) \leq F (z) - X (z) \leftrightarrow X (z) \leq F (z) - Y (z))$
54	53	ralbidva	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (\forall z \in I Y (z) \leq F (z) - X (z) \leftrightarrow \forall z \in I X (z) \leq F (z) - Y (z))$
55		ovexd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) - X (z) \in V$
56	27	feqmptd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y = (z \in I ⟼ Y (z))$
57	17	ffnd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X Fn I$
58		inidm	$⊢ I \cap I = I$
59		eqidd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) = F (z)$
60		eqidd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to X (z) = X (z)$
61	24 57 25 25 58 59 60	offval	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F -_{f} X = (z \in I ⟼ F (z) - X (z))$
62	25 44 55 56 61	ofrfval2	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \leq_{f} (F -_{f} X) \leftrightarrow \forall z \in I Y (z) \leq F (z) - X (z))$
63		ovexd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to F (z) - Y (z) \in V$
64	17	feqmptd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X = (z \in I ⟼ X (z))$
65	27	ffnd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to Y Fn I$
66		eqidd	$⊢ ((φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \land z \in I) \to Y (z) = Y (z)$
67	24 65 25 25 58 59 66	offval	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to F -_{f} Y = (z \in I ⟼ F (z) - Y (z))$
68	25 43 63 64 67	ofrfval2	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (X \leq_{f} (F -_{f} Y) \leftrightarrow \forall z \in I X (z) \leq F (z) - Y (z))$
69	54 62 68	3bitr4d	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \leq_{f} (F -_{f} X) \leftrightarrow X \leq_{f} (F -_{f} Y))$
70	9 69	mpbid	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \leq_{f} (F -_{f} Y)$
71	42 15 70	elrabd	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to X \in \{x \in D \| x \leq_{f} (F -_{f} Y)\}$
72	41 71	jca	$⊢ (φ \land (X \in S \land Y \in \{x \in D \| x \leq_{f} (F -_{f} X)\})) \to (Y \in S \land X \in \{x \in D \| x \leq_{f} (F -_{f} Y)\})$

Metamath Proof Explorer

Theorem gsumbagdiaglem

Proof