Metamath Proof Explorer

Theorem funeldmdif

Description: Two ways of expressing membership in the difference of domains of two nested functions. (Contributed by AV, 27-Oct-2023)

Ref Expression
Assertion funeldmdif ⊢Fun⁡A∧B⊆A→C∈dom⁡A∖dom⁡B↔∃x∈A∖B1st⁡x=C

Proof

Step Hyp Ref Expression
1 funrel ⊢Fun⁡A→Rel⁡A
2 releldmdifi ⊢Rel⁡A∧B⊆A→C∈dom⁡A∖dom⁡B→∃x∈A∖B1st⁡x=C
3 1 2 sylan ⊢Fun⁡A∧B⊆A→C∈dom⁡A∖dom⁡B→∃x∈A∖B1st⁡x=C
4 eldif ⊢x∈A∖B↔x∈A∧¬x∈B
5 1stdm ⊢Rel⁡A∧x∈A→1st⁡x∈dom⁡A
6 5 ex ⊢Rel⁡A→x∈A→1st⁡x∈dom⁡A
7 1 6 syl ⊢Fun⁡A→x∈A→1st⁡x∈dom⁡A
8 7 adantr ⊢Fun⁡A∧B⊆A→x∈A→1st⁡x∈dom⁡A
9 8 com12 ⊢x∈A→Fun⁡A∧B⊆A→1st⁡x∈dom⁡A
10 9 adantr ⊢x∈A∧¬x∈B→Fun⁡A∧B⊆A→1st⁡x∈dom⁡A
11 10 impcom ⊢Fun⁡A∧B⊆A∧x∈A∧¬x∈B→1st⁡x∈dom⁡A
12 funelss ⊢Fun⁡A∧B⊆A∧x∈A→1st⁡x∈dom⁡B→x∈B
13 12 3expa ⊢Fun⁡A∧B⊆A∧x∈A→1st⁡x∈dom⁡B→x∈B
14 13 con3d ⊢Fun⁡A∧B⊆A∧x∈A→¬x∈B→¬1st⁡x∈dom⁡B
15 14 impr ⊢Fun⁡A∧B⊆A∧x∈A∧¬x∈B→¬1st⁡x∈dom⁡B
16 11 15 eldifd ⊢Fun⁡A∧B⊆A∧x∈A∧¬x∈B→1st⁡x∈dom⁡A∖dom⁡B
17 16 3adant3 ⊢Fun⁡A∧B⊆A∧x∈A∧¬x∈B∧1st⁡x=C→1st⁡x∈dom⁡A∖dom⁡B
18 eleq1 ⊢1st⁡x=C→1st⁡x∈dom⁡A∖dom⁡B↔C∈dom⁡A∖dom⁡B
19 18 3ad2ant3 ⊢Fun⁡A∧B⊆A∧x∈A∧¬x∈B∧1st⁡x=C→1st⁡x∈dom⁡A∖dom⁡B↔C∈dom⁡A∖dom⁡B
20 17 19 mpbid ⊢Fun⁡A∧B⊆A∧x∈A∧¬x∈B∧1st⁡x=C→C∈dom⁡A∖dom⁡B
21 20 3exp ⊢Fun⁡A∧B⊆A→x∈A∧¬x∈B→1st⁡x=C→C∈dom⁡A∖dom⁡B
22 4 21 biimtrid ⊢Fun⁡A∧B⊆A→x∈A∖B→1st⁡x=C→C∈dom⁡A∖dom⁡B
23 22 rexlimdv ⊢Fun⁡A∧B⊆A→∃x∈A∖B1st⁡x=C→C∈dom⁡A∖dom⁡B
24 3 23 impbid ⊢Fun⁡A∧B⊆A→C∈dom⁡A∖dom⁡B↔∃x∈A∖B1st⁡x=C