Step | Hyp | Ref
| Expression |
1 | | funfvex 5485 |
. . . . 5
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐺‘𝐴) ∈ V) |
2 | | opeq1 3741 |
. . . . . . 7
⊢ (𝑥 = (𝐺‘𝐴) → 〈𝑥, 𝑦〉 = 〈(𝐺‘𝐴), 𝑦〉) |
3 | 2 | eleq1d 2226 |
. . . . . 6
⊢ (𝑥 = (𝐺‘𝐴) → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹)) |
4 | 3 | ceqsexgv 2841 |
. . . . 5
⊢ ((𝐺‘𝐴) ∈ V → (∃𝑥(𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ 〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹)) |
5 | 1, 4 | syl 14 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (∃𝑥(𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ 〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹)) |
6 | | eqcom 2159 |
. . . . . . 7
⊢ (𝑥 = (𝐺‘𝐴) ↔ (𝐺‘𝐴) = 𝑥) |
7 | | funopfvb 5512 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐺‘𝐴) = 𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
8 | 6, 7 | syl5bb 191 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝑥 = (𝐺‘𝐴) ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
9 | 8 | anbi1d 461 |
. . . . 5
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ (〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
10 | 9 | exbidv 1805 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (∃𝑥(𝑥 = (𝐺‘𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
11 | 5, 10 | bitr3d 189 |
. . 3
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
12 | 11 | exbidv 1805 |
. 2
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (∃𝑦〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
13 | | eldm2g 4782 |
. . 3
⊢ ((𝐺‘𝐴) ∈ V → ((𝐺‘𝐴) ∈ dom 𝐹 ↔ ∃𝑦〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹)) |
14 | 1, 13 | syl 14 |
. 2
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → ((𝐺‘𝐴) ∈ dom 𝐹 ↔ ∃𝑦〈(𝐺‘𝐴), 𝑦〉 ∈ 𝐹)) |
15 | | eldm2g 4782 |
. . . 4
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺))) |
16 | | vex 2715 |
. . . . . 6
⊢ 𝑦 ∈ V |
17 | | opelco2g 4754 |
. . . . . 6
⊢ ((𝐴 ∈ dom 𝐺 ∧ 𝑦 ∈ V) → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
18 | 16, 17 | mpan2 422 |
. . . . 5
⊢ (𝐴 ∈ dom 𝐺 → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
19 | 18 | exbidv 1805 |
. . . 4
⊢ (𝐴 ∈ dom 𝐺 → (∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
20 | 15, 19 | bitrd 187 |
. . 3
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
21 | 20 | adantl 275 |
. 2
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
22 | 12, 14, 21 | 3bitr4rd 220 |
1
⊢ ((Fun
𝐺 ∧ 𝐴 ∈ dom 𝐺) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝐴) ∈ dom 𝐹)) |