Step | Hyp | Ref
| Expression |
1 | | eldm2g 5242 |
. . . 4
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺))) |
2 | | vex 3176 |
. . . . . 6
⊢ 𝑦 ∈ V |
3 | | opelco2g 5211 |
. . . . . 6
⊢ ((𝐴 ∈ dom 𝐺 ∧ 𝑦 ∈ V) → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
4 | 2, 3 | mpan2 703 |
. . . . 5
⊢ (𝐴 ∈ dom 𝐺 → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
5 | 4 | exbidv 1837 |
. . . 4
⊢ (𝐴 ∈ dom 𝐺 → (∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
6 | 1, 5 | bitrd 267 |
. . 3
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
7 | 6 | adantl 481 |
. 2
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
8 | | fvex 6113 |
. . . 4
⊢ (𝐺‘𝐴) ∈ V |
9 | 8 | eldm2 5244 |
. . 3
⊢ ((𝐺‘𝐴) ∈ dom 𝐹 ↔ ∃𝑦〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹) |
10 | | opeq1 4340 |
. . . . . . 7
⊢ (𝑥 = (𝐺‘𝐴) → 〈𝑥, 𝑦〉 = 〈(𝐺‘𝐴), 𝑦〉) |
11 | 10 | eleq1d 2672 |
. . . . . 6
⊢ (𝑥 = (𝐺‘𝐴) → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹)) |
12 | 8, 11 | ceqsexv 3215 |
. . . . 5
⊢
(∃𝑥(𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ 〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹) |
13 | | eqcom 2617 |
. . . . . . . 8
⊢ (𝑥 = (𝐺‘𝐴) ↔ (𝐺‘𝐴) = 𝑥) |
14 | | funopfvb 6149 |
. . . . . . . 8
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐺‘𝐴) = 𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
15 | 13, 14 | syl5bb 271 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝑥 = (𝐺‘𝐴) ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
16 | 15 | anbi1d 737 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ (〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
17 | 16 | exbidv 1837 |
. . . . 5
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (∃𝑥(𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
18 | 12, 17 | syl5bbr 273 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
19 | 18 | exbidv 1837 |
. . 3
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (∃𝑦〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
20 | 9, 19 | syl5bb 271 |
. 2
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐺‘𝐴) ∈ dom 𝐹 ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
21 | 7, 20 | bitr4d 270 |
1
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹)) |