Step | Hyp | Ref
| Expression |
1 | | dfatafv2ex 44285 |
. . . . 5
⊢ (𝐺 defAt 𝐴 → (𝐺''''𝐴) ∈ V) |
2 | | opeq1 4769 |
. . . . . . . 8
⊢ (𝑥 = (𝐺''''𝐴) → 〈𝑥, 𝑦〉 = 〈(𝐺''''𝐴), 𝑦〉) |
3 | 2 | eleq1d 2818 |
. . . . . . 7
⊢ (𝑥 = (𝐺''''𝐴) → (〈𝑥, 𝑦〉 ∈ 𝐹 ↔ 〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹)) |
4 | 3 | ceqsexgv 3553 |
. . . . . 6
⊢ ((𝐺''''𝐴) ∈ V → (∃𝑥(𝑥 = (𝐺''''𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ 〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹)) |
5 | 4 | bicomd 226 |
. . . . 5
⊢ ((𝐺''''𝐴) ∈ V → (〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑥(𝑥 = (𝐺''''𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
6 | 1, 5 | syl 17 |
. . . 4
⊢ (𝐺 defAt 𝐴 → (〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑥(𝑥 = (𝐺''''𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
7 | | eqcom 2746 |
. . . . . . 7
⊢ (𝑥 = (𝐺''''𝐴) ↔ (𝐺''''𝐴) = 𝑥) |
8 | | dfatopafv2b 44318 |
. . . . . . . 8
⊢ ((𝐺 defAt 𝐴 ∧ 𝑥 ∈ V) → ((𝐺''''𝐴) = 𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
9 | 8 | elvd 3407 |
. . . . . . 7
⊢ (𝐺 defAt 𝐴 → ((𝐺''''𝐴) = 𝑥 ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
10 | 7, 9 | syl5bb 286 |
. . . . . 6
⊢ (𝐺 defAt 𝐴 → (𝑥 = (𝐺''''𝐴) ↔ 〈𝐴, 𝑥〉 ∈ 𝐺)) |
11 | 10 | anbi1d 633 |
. . . . 5
⊢ (𝐺 defAt 𝐴 → ((𝑥 = (𝐺''''𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ (〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
12 | 11 | exbidv 1928 |
. . . 4
⊢ (𝐺 defAt 𝐴 → (∃𝑥(𝑥 = (𝐺''''𝐴) ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
13 | 6, 12 | bitrd 282 |
. . 3
⊢ (𝐺 defAt 𝐴 → (〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
14 | 13 | exbidv 1928 |
. 2
⊢ (𝐺 defAt 𝐴 → (∃𝑦〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹 ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
15 | | eldm2g 5752 |
. . 3
⊢ ((𝐺''''𝐴) ∈ V → ((𝐺''''𝐴) ∈ dom 𝐹 ↔ ∃𝑦〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹)) |
16 | 1, 15 | syl 17 |
. 2
⊢ (𝐺 defAt 𝐴 → ((𝐺''''𝐴) ∈ dom 𝐹 ↔ ∃𝑦〈(𝐺''''𝐴), 𝑦〉 ∈ 𝐹)) |
17 | | df-dfat 44191 |
. . 3
⊢ (𝐺 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝐴}))) |
18 | | eldm2g 5752 |
. . . . 5
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺))) |
19 | | opelco2g 5720 |
. . . . . . 7
⊢ ((𝐴 ∈ dom 𝐺 ∧ 𝑦 ∈ V) → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
20 | 19 | elvd 3407 |
. . . . . 6
⊢ (𝐴 ∈ dom 𝐺 → (〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
21 | 20 | exbidv 1928 |
. . . . 5
⊢ (𝐴 ∈ dom 𝐺 → (∃𝑦〈𝐴, 𝑦〉 ∈ (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
22 | 18, 21 | bitrd 282 |
. . . 4
⊢ (𝐴 ∈ dom 𝐺 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
23 | 22 | adantr 484 |
. . 3
⊢ ((𝐴 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝐴})) → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
24 | 17, 23 | sylbi 220 |
. 2
⊢ (𝐺 defAt 𝐴 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ ∃𝑦∃𝑥(〈𝐴, 𝑥〉 ∈ 𝐺 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹))) |
25 | 14, 16, 24 | 3bitr4rd 315 |
1
⊢ (𝐺 defAt 𝐴 → (𝐴 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺''''𝐴) ∈ dom 𝐹)) |