Step |
Hyp |
Ref |
Expression |
1 |
|
itg2val.1 |
⊢ 𝐿 = { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } |
2 |
1
|
eleq2i |
⊢ ( 𝐴 ∈ 𝐿 ↔ 𝐴 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ) |
3 |
|
simpr |
⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) → 𝐴 = ( ∫1 ‘ 𝑔 ) ) |
4 |
|
fvex |
⊢ ( ∫1 ‘ 𝑔 ) ∈ V |
5 |
3 4
|
eqeltrdi |
⊢ ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) → 𝐴 ∈ V ) |
6 |
5
|
rexlimivw |
⊢ ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) → 𝐴 ∈ V ) |
7 |
|
eqeq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ( ∫1 ‘ 𝑔 ) ↔ 𝐴 = ( ∫1 ‘ 𝑔 ) ) ) |
8 |
7
|
anbi2d |
⊢ ( 𝑥 = 𝐴 → ( ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) ) ) |
9 |
8
|
rexbidv |
⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) ) ) |
10 |
6 9
|
elab3 |
⊢ ( 𝐴 ∈ { 𝑥 ∣ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝑥 = ( ∫1 ‘ 𝑔 ) ) } ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) ) |
11 |
2 10
|
bitri |
⊢ ( 𝐴 ∈ 𝐿 ↔ ∃ 𝑔 ∈ dom ∫1 ( 𝑔 ∘r ≤ 𝐹 ∧ 𝐴 = ( ∫1 ‘ 𝑔 ) ) ) |