| Step | Hyp | Ref
| Expression |
| 1 | | eldm2g 5910 |
. . . 4
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺))) |
| 2 | | opelco2g 5878 |
. . . . . 6
⊢ ((𝐴 ∈ dom 𝐺 ∧ 𝑦 ∈ V) → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 3 | 2 | elvd 3486 |
. . . . 5
⊢ (𝐴 ∈ dom 𝐺 → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 4 | 3 | exbidv 1921 |
. . . 4
⊢ (𝐴 ∈ dom 𝐺 → (∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 5 | 1, 4 | bitrd 279 |
. . 3
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 6 | 5 | adantl 481 |
. 2
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 7 | | fvex 6919 |
. . . 4
⊢ (𝐺‘𝐴) ∈ V |
| 8 | 7 | eldm2 5912 |
. . 3
⊢ ((𝐺‘𝐴) ∈ dom 𝐹 ↔ ∃𝑦〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹) |
| 9 | | opeq1 4873 |
. . . . . . 7
⊢ (𝑥 = (𝐺‘𝐴) → 〈𝑥, 𝑦〉 = 〈(𝐺‘𝐴), 𝑦〉) |
| 10 | 9 | eleq1d 2826 |
. . . . . 6
⊢ (𝑥 = (𝐺‘𝐴) → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹)) |
| 11 | 7, 10 | ceqsexv 3532 |
. . . . 5
⊢
(∃𝑥(𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ 〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹) |
| 12 | | eqcom 2744 |
. . . . . . . 8
⊢ (𝑥 = (𝐺‘𝐴) ↔ (𝐺‘𝐴) = 𝑥) |
| 13 | | funopfvb 6963 |
. . . . . . . 8
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐺‘𝐴) = 𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
| 14 | 12, 13 | bitrid 283 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝑥 = (𝐺‘𝐴) ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
| 15 | 14 | anbi1d 631 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ (〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 16 | 15 | exbidv 1921 |
. . . . 5
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (∃𝑥(𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 17 | 11, 16 | bitr3id 285 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 18 | 17 | exbidv 1921 |
. . 3
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (∃𝑦〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 19 | 8, 18 | bitrid 283 |
. 2
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐺‘𝐴) ∈ dom 𝐹 ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
| 20 | 6, 19 | bitr4d 282 |
1
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹)) |