itg2l

Description: Elementhood in the set L of lower sums of the integral. (Contributed by Mario Carneiro, 28-Jun-2014)

		Ref	Expression
	Hypothesis	itg2val.1	$⊢ L = \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
	Assertion	itg2l	$⊢ A \in L \leftrightarrow \exists g \in dom \int^{1} (g \leq_{f} F \land A = \int^{1} (g))$

Step	Hyp	Ref	Expression
1		itg2val.1	$⊢ L = \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
2	1	eleq2i	$⊢ A \in L \leftrightarrow A \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\}$
3		simpr	$⊢ (g \leq_{f} F \land A = \int^{1} (g)) \to A = \int^{1} (g)$
4		fvex	$⊢ \int^{1} (g) \in V$
5	3 4	eqeltrdi	$⊢ (g \leq_{f} F \land A = \int^{1} (g)) \to A \in V$
6	5	rexlimivw	$⊢ \exists g \in dom \int^{1} (g \leq_{f} F \land A = \int^{1} (g)) \to A \in V$
7		eqeq1	$⊢ x = A \to (x = \int^{1} (g) \leftrightarrow A = \int^{1} (g))$
8	7	anbi2d	$⊢ x = A \to ((g \leq_{f} F \land x = \int^{1} (g)) \leftrightarrow (g \leq_{f} F \land A = \int^{1} (g)))$
9	8	rexbidv	$⊢ x = A \to (\exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g)) \leftrightarrow \exists g \in dom \int^{1} (g \leq_{f} F \land A = \int^{1} (g)))$
10	6 9	elab3	$⊢ A \in \{x \| \exists g \in dom \int^{1} (g \leq_{f} F \land x = \int^{1} (g))\} \leftrightarrow \exists g \in dom \int^{1} (g \leq_{f} F \land A = \int^{1} (g))$
11	2 10	bitri	$⊢ A \in L \leftrightarrow \exists g \in dom \int^{1} (g \leq_{f} F \land A = \int^{1} (g))$

Metamath Proof Explorer