itg2lr

Description: Sufficient condition for elementhood in the set L . (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	itg2lr	$⊢ (G \in dom \int^{1} \land G \leq_{f} F) \to \int^{1} (G) \in L$

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		eqid	$⊢ \int^{1} (G) = \int^{1} (G)$
3		breq1	$⊢ g = G \to (g \leq_{f} F \leftrightarrow G \leq_{f} F)$
4		fveq2	$⊢ g = G \to \int^{1} (g) = \int^{1} (G)$
5	4	eqeq2d	$⊢ g = G \to (\int^{1} (G) = \int^{1} (g) \leftrightarrow \int^{1} (G) = \int^{1} (G))$
6	3 5	anbi12d	$⊢ g = G \to ((g \leq_{f} F \land \int^{1} (G) = \int^{1} (g)) \leftrightarrow (G \leq_{f} F \land \int^{1} (G) = \int^{1} (G)))$
7	6	rspcev	$⊢ (G \in dom \int^{1} \land (G \leq_{f} F \land \int^{1} (G) = \int^{1} (G))) \to \exists g \in dom \int^{1} (g \leq_{f} F \land \int^{1} (G) = \int^{1} (g))$
8	2 7	mpanr2	$⊢ (G \in dom \int^{1} \land G \leq_{f} F) \to \exists g \in dom \int^{1} (g \leq_{f} F \land \int^{1} (G) = \int^{1} (g))$
9	1	itg2l	$⊢ \int^{1} (G) \in L \leftrightarrow \exists g \in dom \int^{1} (g \leq_{f} F \land \int^{1} (G) = \int^{1} (g))$
10	8 9	sylibr	$⊢ (G \in dom \int^{1} \land G \leq_{f} F) \to \int^{1} (G) \in L$

Metamath Proof Explorer