Theorem itg2lr

Description: Sufficient condition for elementhood in the set L . (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Hypothesis	itg2val.1	⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
Assertion	itg2lr	⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐺 ) ∈ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		itg2val.1	⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) }
2		eqid	⊢ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝐺 )
3		breq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∘r ≤ 𝐹 ↔ 𝐺 ∘r ≤ 𝐹 ) )
4		fveq2	⊢ ( 𝑔 = 𝐺 → ( ∫1 ‘ 𝑔 ) = ( ∫1 ‘ 𝐺 ) )
5	4	eqeq2d	⊢ ( 𝑔 = 𝐺 → ( ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝑔 ) ↔ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝐺 ) ) )
6	3 5	anbi12d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑔 ∘r ≤ 𝐹 ∧ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝑔 ) ) ↔ ( 𝐺 ∘r ≤ 𝐹 ∧ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝐺 ) ) ) )
7	6	rspcev	⊢ ( ( 𝐺 ∈ dom ∫1 ∧ ( 𝐺 ∘r ≤ 𝐹 ∧ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝐺 ) ) ) → ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝑔 ) ) )
8	2 7	mpanr2	⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝑔 ) ) )
9	1	itg2l	⊢ ( ( ∫1 ‘ 𝐺 ) ∈ 𝐿 ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ ( ∫1 ‘ 𝐺 ) = ( ∫1 ‘ 𝑔 ) ) )
10	8 9	sylibr	⊢ ( ( 𝐺 ∈ dom ∫1 ∧ 𝐺 ∘r ≤ 𝐹 ) → ( ∫1 ‘ 𝐺 ) ∈ 𝐿 )