This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐺 ) ∈ 𝐿 )