Step | Hyp | Ref
| Expression |
1 | | dfdfat2 44201 |
. . . 4
⊢ (𝐹 defAt (𝐺''''𝑋) ↔ ((𝐺''''𝑋) ∈ dom 𝐹 ∧ ∃!𝑦(𝐺''''𝑋)𝐹𝑦)) |
2 | | eqidd 2740 |
. . . . . . . . . 10
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝐺''''𝑋) = (𝐺''''𝑋)) |
3 | | df-dfat 44192 |
. . . . . . . . . . . 12
⊢ (𝐹 defAt (𝐺''''𝑋) ↔ ((𝐺''''𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺''''𝑋)}))) |
4 | 3 | simplbi 501 |
. . . . . . . . . . 11
⊢ (𝐹 defAt (𝐺''''𝑋) → (𝐺''''𝑋) ∈ dom 𝐹) |
5 | | dfatbrafv2b 44318 |
. . . . . . . . . . 11
⊢ ((𝐺 defAt 𝑋 ∧ (𝐺''''𝑋) ∈ dom 𝐹) → ((𝐺''''𝑋) = (𝐺''''𝑋) ↔ 𝑋𝐺(𝐺''''𝑋))) |
6 | 4, 5 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝐺''''𝑋) = (𝐺''''𝑋) ↔ 𝑋𝐺(𝐺''''𝑋))) |
7 | 2, 6 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → 𝑋𝐺(𝐺''''𝑋)) |
8 | | eqidd 2740 |
. . . . . . . . . 10
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝐹''''(𝐺''''𝑋)) = (𝐹''''(𝐺''''𝑋))) |
9 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → 𝐹 defAt (𝐺''''𝑋)) |
10 | | dfatafv2ex 44286 |
. . . . . . . . . . . 12
⊢ (𝐹 defAt (𝐺''''𝑋) → (𝐹''''(𝐺''''𝑋)) ∈ V) |
11 | 10 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝐹''''(𝐺''''𝑋)) ∈ V) |
12 | | dfatbrafv2b 44318 |
. . . . . . . . . . 11
⊢ ((𝐹 defAt (𝐺''''𝑋) ∧ (𝐹''''(𝐺''''𝑋)) ∈ V) → ((𝐹''''(𝐺''''𝑋)) = (𝐹''''(𝐺''''𝑋)) ↔ (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋)))) |
13 | 9, 11, 12 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝐹''''(𝐺''''𝑋)) = (𝐹''''(𝐺''''𝑋)) ↔ (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋)))) |
14 | 8, 13 | mpbid 235 |
. . . . . . . . 9
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋))) |
15 | 4 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝐺''''𝑋) ∈ dom 𝐹) |
16 | | breq2 5044 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐺''''𝑋) → (𝑋𝐺𝑧 ↔ 𝑋𝐺(𝐺''''𝑋))) |
17 | 16 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑦 = (𝐹''''(𝐺''''𝑋)) ∧ 𝑧 = (𝐺''''𝑋)) → (𝑋𝐺𝑧 ↔ 𝑋𝐺(𝐺''''𝑋))) |
18 | | breq12 5045 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = (𝐺''''𝑋) ∧ 𝑦 = (𝐹''''(𝐺''''𝑋))) → (𝑧𝐹𝑦 ↔ (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋)))) |
19 | 18 | ancoms 462 |
. . . . . . . . . . . 12
⊢ ((𝑦 = (𝐹''''(𝐺''''𝑋)) ∧ 𝑧 = (𝐺''''𝑋)) → (𝑧𝐹𝑦 ↔ (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋)))) |
20 | 17, 19 | anbi12d 634 |
. . . . . . . . . . 11
⊢ ((𝑦 = (𝐹''''(𝐺''''𝑋)) ∧ 𝑧 = (𝐺''''𝑋)) → ((𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦) ↔ (𝑋𝐺(𝐺''''𝑋) ∧ (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋))))) |
21 | 20 | spc2egv 3506 |
. . . . . . . . . 10
⊢ (((𝐹''''(𝐺''''𝑋)) ∈ V ∧ (𝐺''''𝑋) ∈ dom 𝐹) → ((𝑋𝐺(𝐺''''𝑋) ∧ (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋))) → ∃𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
22 | 11, 15, 21 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝑋𝐺(𝐺''''𝑋) ∧ (𝐺''''𝑋)𝐹(𝐹''''(𝐺''''𝑋))) → ∃𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
23 | 7, 14, 22 | mp2and 699 |
. . . . . . . 8
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)) |
24 | | dfdfat2 44201 |
. . . . . . . . . . . . . 14
⊢ (𝐺 defAt 𝑋 ↔ (𝑋 ∈ dom 𝐺 ∧ ∃!𝑧 𝑋𝐺𝑧)) |
25 | | tz6.12c-afv2 44315 |
. . . . . . . . . . . . . . 15
⊢
(∃!𝑧 𝑋𝐺𝑧 → ((𝐺''''𝑋) = 𝑧 ↔ 𝑋𝐺𝑧)) |
26 | 25 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈ dom 𝐺 ∧ ∃!𝑧 𝑋𝐺𝑧) → ((𝐺''''𝑋) = 𝑧 ↔ 𝑋𝐺𝑧)) |
27 | 24, 26 | sylbi 220 |
. . . . . . . . . . . . 13
⊢ (𝐺 defAt 𝑋 → ((𝐺''''𝑋) = 𝑧 ↔ 𝑋𝐺𝑧)) |
28 | 27 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝐺''''𝑋) = 𝑧 ↔ 𝑋𝐺𝑧)) |
29 | | breq1 5043 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺''''𝑋) = 𝑧 → ((𝐺''''𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦)) |
30 | 29 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 defAt (𝐺''''𝑋) ∧ (𝐺''''𝑋) = 𝑧) → ((𝐺''''𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦)) |
31 | 30 | exbiri 811 |
. . . . . . . . . . . . 13
⊢ (𝐹 defAt (𝐺''''𝑋) → ((𝐺''''𝑋) = 𝑧 → (𝑧𝐹𝑦 → (𝐺''''𝑋)𝐹𝑦))) |
32 | 31 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝐺''''𝑋) = 𝑧 → (𝑧𝐹𝑦 → (𝐺''''𝑋)𝐹𝑦))) |
33 | 28, 32 | sylbird 263 |
. . . . . . . . . . 11
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝑋𝐺𝑧 → (𝑧𝐹𝑦 → (𝐺''''𝑋)𝐹𝑦))) |
34 | 33 | impd 414 |
. . . . . . . . . 10
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦) → (𝐺''''𝑋)𝐹𝑦)) |
35 | 34 | exlimdv 1940 |
. . . . . . . . 9
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦) → (𝐺''''𝑋)𝐹𝑦)) |
36 | 35 | alrimiv 1934 |
. . . . . . . 8
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∀𝑦(∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦) → (𝐺''''𝑋)𝐹𝑦)) |
37 | | euim 2621 |
. . . . . . . 8
⊢
((∃𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦) ∧ ∀𝑦(∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦) → (𝐺''''𝑋)𝐹𝑦)) → (∃!𝑦(𝐺''''𝑋)𝐹𝑦 → ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
38 | 23, 36, 37 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (∃!𝑦(𝐺''''𝑋)𝐹𝑦 → ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
39 | 38 | com12 32 |
. . . . . 6
⊢
(∃!𝑦(𝐺''''𝑋)𝐹𝑦 → ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
40 | 39 | adantl 485 |
. . . . 5
⊢ (((𝐺''''𝑋) ∈ dom 𝐹 ∧ ∃!𝑦(𝐺''''𝑋)𝐹𝑦) → ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
41 | 40 | adantl 485 |
. . . 4
⊢ ((𝐺 defAt 𝑋 ∧ ((𝐺''''𝑋) ∈ dom 𝐹 ∧ ∃!𝑦(𝐺''''𝑋)𝐹𝑦)) → ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
42 | 1, 41 | sylan2b 597 |
. . 3
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
43 | 42 | pm2.43i 52 |
. 2
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)) |
44 | | df-dfat 44192 |
. . . . 5
⊢ (𝐺 defAt 𝑋 ↔ (𝑋 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝑋}))) |
45 | 44 | simplbi 501 |
. . . 4
⊢ (𝐺 defAt 𝑋 → 𝑋 ∈ dom 𝐺) |
46 | | vex 3404 |
. . . . 5
⊢ 𝑦 ∈ V |
47 | 46 | a1i 11 |
. . . 4
⊢ (𝐹 defAt (𝐺''''𝑋) → 𝑦 ∈ V) |
48 | | brcog 5719 |
. . . 4
⊢ ((𝑋 ∈ dom 𝐺 ∧ 𝑦 ∈ V) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
49 | 45, 47, 48 | syl2an 599 |
. . 3
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
50 | 49 | eubidv 2588 |
. 2
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → (∃!𝑦 𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃!𝑦∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) |
51 | 43, 50 | mpbird 260 |
1
⊢ ((𝐺 defAt 𝑋 ∧ 𝐹 defAt (𝐺''''𝑋)) → ∃!𝑦 𝑋(𝐹 ∘ 𝐺)𝑦) |