| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relres 6023 | . . 3
⊢ Rel
(𝐹 ↾ {(𝐺‘𝑋)}) | 
| 2 | 1 | a1i 11 | . 2
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Rel (𝐹 ↾ {(𝐺‘𝑋)})) | 
| 3 |  | dmfco 7005 | . . . . . . . . 9
⊢ ((Fun
𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹)) | 
| 4 | 3 | biimpd 229 | . . . . . . . 8
⊢ ((Fun
𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹)) | 
| 5 | 4 | funfni 6674 | . . . . . . 7
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹)) | 
| 6 |  | dmressnsn 6041 | . . . . . . . 8
⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)}) | 
| 7 |  | eleq2 2830 | . . . . . . . . . 10
⊢ (dom
(𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) ↔ 𝑥 ∈ {(𝐺‘𝑋)})) | 
| 8 |  | velsn 4642 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {(𝐺‘𝑋)} ↔ 𝑥 = (𝐺‘𝑋)) | 
| 9 |  | dmressnsn 6041 | . . . . . . . . . . . . . . . . 17
⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋}) | 
| 10 |  | dffun7 6593 | . . . . . . . . . . . . . . . . . . 19
⊢ (Fun
((𝐹 ∘ 𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹 ∘ 𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)) | 
| 11 |  | snidg 4660 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → 𝑋 ∈ {𝑋}) | 
| 12 | 11 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ {𝑋}) | 
| 13 |  | eleq2 2830 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ({𝑋} = dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋}))) | 
| 14 | 13 | eqcoms 2745 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋}))) | 
| 15 | 14 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋}))) | 
| 16 | 12, 15 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})) | 
| 17 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐺‘𝑋) ∈ V | 
| 18 | 17 | isseti 3498 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
∃𝑧 𝑧 = (𝐺‘𝑋) | 
| 19 |  | eqcom 2744 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 = (𝐺‘𝑋) ↔ (𝐺‘𝑋) = 𝑧) | 
| 20 |  | fnbrfvb 6959 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋) = 𝑧 ↔ 𝑋𝐺𝑧)) | 
| 21 | 19, 20 | bitrid 283 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) ↔ 𝑋𝐺𝑧)) | 
| 22 | 21 | biimpd 229 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) → 𝑋𝐺𝑧)) | 
| 23 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐺‘𝑋) = 𝑧 → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦)) | 
| 24 | 23 | eqcoms 2745 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 = (𝐺‘𝑋) → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦)) | 
| 25 | 24 | biimpcd 249 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐺‘𝑋)𝐹𝑦 → (𝑧 = (𝐺‘𝑋) → 𝑧𝐹𝑦)) | 
| 26 | 22, 25 | anim12ii 618 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑧 = (𝐺‘𝑋) → (𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) | 
| 27 | 26 | eximdv 1917 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺‘𝑋) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) | 
| 28 | 18, 27 | mpi 20 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)) | 
| 29 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴) | 
| 30 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝑦 ∈ V | 
| 31 |  | brcog 5877 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ V) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) | 
| 32 | 29, 30, 31 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) | 
| 33 | 32 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))) | 
| 34 | 28, 33 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋(𝐹 ∘ 𝐺)𝑦) | 
| 35 | 30 | brresi 6006 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹 ∘ 𝐺)𝑦)) | 
| 36 |  | snidg 4660 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ {𝑋}) | 
| 37 | 36 | biantrurd 532 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑋 ∈ 𝐴 → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹 ∘ 𝐺)𝑦))) | 
| 38 | 35, 37 | bitr4id 290 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑋 ∈ 𝐴 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦)) | 
| 39 | 38 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦)) | 
| 40 | 34, 39 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦) | 
| 41 | 40 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)) | 
| 42 | 41 | adantl 481 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)) | 
| 43 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑋 = 𝑥 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)) | 
| 44 | 43 | eqcoms 2745 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = 𝑋 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)) | 
| 45 | 44 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)) | 
| 46 | 42, 45 | sylibd 239 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)) | 
| 47 | 46 | moimdv 2546 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)) | 
| 48 | 47 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))) | 
| 49 | 48 | com23 86 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))) | 
| 50 | 16, 49 | rspcimdv 3612 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))) | 
| 51 | 50 | ex 412 | . . . . . . . . . . . . . . . . . . . 20
⊢ (dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))) | 
| 52 | 51 | com13 88 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))) | 
| 53 | 10, 52 | simplbiim 504 | . . . . . . . . . . . . . . . . . 18
⊢ (Fun
((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))) | 
| 54 | 53 | com13 88 | . . . . . . . . . . . . . . . . 17
⊢ (dom
((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))) | 
| 55 | 9, 54 | mpcom 38 | . . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))) | 
| 56 | 55 | imp31 417 | . . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦) | 
| 57 | 17 | snid 4662 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)} | 
| 58 | 57 | biantrur 530 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)) | 
| 59 | 58 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))) | 
| 60 | 59 | mobidv 2549 | . . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦(𝐺‘𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))) | 
| 61 | 56, 60 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)) | 
| 62 | 61 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)) | 
| 63 |  | breq1 5146 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = (𝐺‘𝑋) → (𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ (𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 64 | 30 | brresi 6006 | . . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)) | 
| 65 | 63, 64 | bitr2di 288 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝐺‘𝑋) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 66 | 65 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 67 | 66 | mobidv 2549 | . . . . . . . . . . . . 13
⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 68 | 62, 67 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦) | 
| 69 | 68 | ex 412 | . . . . . . . . . . 11
⊢ (𝑥 = (𝐺‘𝑋) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 70 | 8, 69 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑥 ∈ {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 71 | 7, 70 | biimtrdi 253 | . . . . . . . . 9
⊢ (dom
(𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))) | 
| 72 | 71 | com23 86 | . . . . . . . 8
⊢ (dom
(𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))) | 
| 73 | 6, 72 | syl 17 | . . . . . . 7
⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))) | 
| 74 | 5, 73 | syl6com 37 | . . . . . 6
⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))) | 
| 75 | 74 | a1d 25 | . . . . 5
⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))))) | 
| 76 | 75 | imp31 417 | . . . 4
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))) | 
| 77 | 76 | pm2.43i 52 | . . 3
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 78 | 77 | ralrimiv 3145 | . 2
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦) | 
| 79 |  | dffun7 6593 | . 2
⊢ (Fun
(𝐹 ↾ {(𝐺‘𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺‘𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)) | 
| 80 | 2, 78, 79 | sylanbrc 583 | 1
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)})) |