Metamath Proof Explorer

Theorem dfatcolem

Description: Lemma for dfatco . (Contributed by AV, 8-Sep-2022)

Ref Expression
Assertion dfatcolem ⊢ G defAt X ∧ F defAt G '''' X → ∃! y X F ∘ G y

Proof

Step Hyp Ref Expression
1 dfdfat2 ⊢ F defAt G '''' X ↔ G '''' X ∈ dom ⁡ F ∧ ∃! y G '''' X F y
2 eqidd ⊢ G defAt X ∧ F defAt G '''' X → G '''' X = G '''' X
3 df-dfat ⊢ F defAt G '''' X ↔ G '''' X ∈ dom ⁡ F ∧ Fun ⁡ F ↾ G '''' X
4 3 simplbi ⊢ F defAt G '''' X → G '''' X ∈ dom ⁡ F
5 dfatbrafv2b ⊢ G defAt X ∧ G '''' X ∈ dom ⁡ F → G '''' X = G '''' X ↔ X G G '''' X
6 4 5 sylan2 ⊢ G defAt X ∧ F defAt G '''' X → G '''' X = G '''' X ↔ X G G '''' X
7 2 6 mpbid ⊢ G defAt X ∧ F defAt G '''' X → X G G '''' X
8 eqidd ⊢ G defAt X ∧ F defAt G '''' X → F '''' G '''' X = F '''' G '''' X
9 simpr ⊢ G defAt X ∧ F defAt G '''' X → F defAt G '''' X
10 dfatafv2ex ⊢ F defAt G '''' X → F '''' G '''' X ∈ V
11 10 adantl ⊢ G defAt X ∧ F defAt G '''' X → F '''' G '''' X ∈ V
12 dfatbrafv2b ⊢ F defAt G '''' X ∧ F '''' G '''' X ∈ V → F '''' G '''' X = F '''' G '''' X ↔ G '''' X F F '''' G '''' X
13 9 11 12 syl2anc ⊢ G defAt X ∧ F defAt G '''' X → F '''' G '''' X = F '''' G '''' X ↔ G '''' X F F '''' G '''' X
14 8 13 mpbid ⊢ G defAt X ∧ F defAt G '''' X → G '''' X F F '''' G '''' X
15 4 adantl ⊢ G defAt X ∧ F defAt G '''' X → G '''' X ∈ dom ⁡ F
16 breq2 ⊢ z = G '''' X → X G z ↔ X G G '''' X
17 16 adantl ⊢ y = F '''' G '''' X ∧ z = G '''' X → X G z ↔ X G G '''' X
18 breq12 ⊢ z = G '''' X ∧ y = F '''' G '''' X → z F y ↔ G '''' X F F '''' G '''' X
19 18 ancoms ⊢ y = F '''' G '''' X ∧ z = G '''' X → z F y ↔ G '''' X F F '''' G '''' X
20 17 19 anbi12d ⊢ y = F '''' G '''' X ∧ z = G '''' X → X G z ∧ z F y ↔ X G G '''' X ∧ G '''' X F F '''' G '''' X
21 20 spc2egv ⊢ F '''' G '''' X ∈ V ∧ G '''' X ∈ dom ⁡ F → X G G '''' X ∧ G '''' X F F '''' G '''' X → ∃ y ∃ z X G z ∧ z F y
22 11 15 21 syl2anc ⊢ G defAt X ∧ F defAt G '''' X → X G G '''' X ∧ G '''' X F F '''' G '''' X → ∃ y ∃ z X G z ∧ z F y
23 7 14 22 mp2and ⊢ G defAt X ∧ F defAt G '''' X → ∃ y ∃ z X G z ∧ z F y
24 dfdfat2 ⊢ G defAt X ↔ X ∈ dom ⁡ G ∧ ∃! z X G z
25 tz6.12c-afv2 ⊢ ∃! z X G z → G '''' X = z ↔ X G z
26 25 adantl ⊢ X ∈ dom ⁡ G ∧ ∃! z X G z → G '''' X = z ↔ X G z
27 24 26 sylbi ⊢ G defAt X → G '''' X = z ↔ X G z
28 27 adantr ⊢ G defAt X ∧ F defAt G '''' X → G '''' X = z ↔ X G z
29 breq1 ⊢ G '''' X = z → G '''' X F y ↔ z F y
30 29 adantl ⊢ F defAt G '''' X ∧ G '''' X = z → G '''' X F y ↔ z F y
31 30 exbiri ⊢ F defAt G '''' X → G '''' X = z → z F y → G '''' X F y
32 31 adantl ⊢ G defAt X ∧ F defAt G '''' X → G '''' X = z → z F y → G '''' X F y
33 28 32 sylbird ⊢ G defAt X ∧ F defAt G '''' X → X G z → z F y → G '''' X F y
34 33 impd ⊢ G defAt X ∧ F defAt G '''' X → X G z ∧ z F y → G '''' X F y
35 34 exlimdv ⊢ G defAt X ∧ F defAt G '''' X → ∃ z X G z ∧ z F y → G '''' X F y
36 35 alrimiv ⊢ G defAt X ∧ F defAt G '''' X → ∀ y ∃ z X G z ∧ z F y → G '''' X F y
37 euim ⊢ ∃ y ∃ z X G z ∧ z F y ∧ ∀ y ∃ z X G z ∧ z F y → G '''' X F y → ∃! y G '''' X F y → ∃! y ∃ z X G z ∧ z F y
38 23 36 37 syl2anc ⊢ G defAt X ∧ F defAt G '''' X → ∃! y G '''' X F y → ∃! y ∃ z X G z ∧ z F y
39 38 com12 ⊢ ∃! y G '''' X F y → G defAt X ∧ F defAt G '''' X → ∃! y ∃ z X G z ∧ z F y
40 39 adantl ⊢ G '''' X ∈ dom ⁡ F ∧ ∃! y G '''' X F y → G defAt X ∧ F defAt G '''' X → ∃! y ∃ z X G z ∧ z F y
41 40 adantl ⊢ G defAt X ∧ G '''' X ∈ dom ⁡ F ∧ ∃! y G '''' X F y → G defAt X ∧ F defAt G '''' X → ∃! y ∃ z X G z ∧ z F y
42 1 41 sylan2b ⊢ G defAt X ∧ F defAt G '''' X → G defAt X ∧ F defAt G '''' X → ∃! y ∃ z X G z ∧ z F y
43 42 pm2.43i ⊢ G defAt X ∧ F defAt G '''' X → ∃! y ∃ z X G z ∧ z F y
44 df-dfat ⊢ G defAt X ↔ X ∈ dom ⁡ G ∧ Fun ⁡ G ↾ X
45 44 simplbi ⊢ G defAt X → X ∈ dom ⁡ G
46 vex ⊢ y ∈ V
47 46 a1i ⊢ F defAt G '''' X → y ∈ V
48 brcog ⊢ X ∈ dom ⁡ G ∧ y ∈ V → X F ∘ G y ↔ ∃ z X G z ∧ z F y
49 45 47 48 syl2an ⊢ G defAt X ∧ F defAt G '''' X → X F ∘ G y ↔ ∃ z X G z ∧ z F y
50 49 eubidv ⊢ G defAt X ∧ F defAt G '''' X → ∃! y X F ∘ G y ↔ ∃! y ∃ z X G z ∧ z F y
51 43 50 mpbird ⊢ G defAt X ∧ F defAt G '''' X → ∃! y X F ∘ G y