Metamath Proof Explorer

Theorem dfatcolem

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

Ref Expression
Assertion dfatcolem ( ( 𝐺 defAt 𝑋 ∧ 𝐹 defAt ( 𝐺 '''' 𝑋 ) ) → ∃! 𝑦 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 )

Proof

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