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 ∖ B 1 st ⁡ 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 ∖ B 1 st ⁡ x = C
3 1 2 sylan ⊢ Fun ⁡ A ∧ B ⊆ A → C ∈ dom ⁡ A ∖ dom ⁡ B → ∃ x ∈ A ∖ B 1 st ⁡ x = C
4 eldif ⊢ x ∈ A ∖ B ↔ x ∈ A ∧ ¬ x ∈ B
5 1stdm ⊢ Rel ⁡ A ∧ x ∈ A → 1 st ⁡ x ∈ dom ⁡ A
6 5 ex ⊢ Rel ⁡ A → x ∈ A → 1 st ⁡ x ∈ dom ⁡ A
7 1 6 syl ⊢ Fun ⁡ A → x ∈ A → 1 st ⁡ x ∈ dom ⁡ A
8 7 adantr ⊢ Fun ⁡ A ∧ B ⊆ A → x ∈ A → 1 st ⁡ x ∈ dom ⁡ A
9 8 com12 ⊢ x ∈ A → Fun ⁡ A ∧ B ⊆ A → 1 st ⁡ x ∈ dom ⁡ A
10 9 adantr ⊢ x ∈ A ∧ ¬ x ∈ B → Fun ⁡ A ∧ B ⊆ A → 1 st ⁡ x ∈ dom ⁡ A
11 10 impcom ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A ∧ ¬ x ∈ B → 1 st ⁡ x ∈ dom ⁡ A
12 funelss ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A → 1 st ⁡ x ∈ dom ⁡ B → x ∈ B
13 12 3expa ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A → 1 st ⁡ x ∈ dom ⁡ B → x ∈ B
14 13 con3d ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A → ¬ x ∈ B → ¬ 1 st ⁡ x ∈ dom ⁡ B
15 14 impr ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A ∧ ¬ x ∈ B → ¬ 1 st ⁡ x ∈ dom ⁡ B
16 11 15 eldifd ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A ∧ ¬ x ∈ B → 1 st ⁡ x ∈ dom ⁡ A ∖ dom ⁡ B
17 16 3adant3 ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A ∧ ¬ x ∈ B ∧ 1 st ⁡ x = C → 1 st ⁡ x ∈ dom ⁡ A ∖ dom ⁡ B
18 eleq1 ⊢ 1 st ⁡ x = C → 1 st ⁡ x ∈ dom ⁡ A ∖ dom ⁡ B ↔ C ∈ dom ⁡ A ∖ dom ⁡ B
19 18 3ad2ant3 ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A ∧ ¬ x ∈ B ∧ 1 st ⁡ x = C → 1 st ⁡ x ∈ dom ⁡ A ∖ dom ⁡ B ↔ C ∈ dom ⁡ A ∖ dom ⁡ B
20 17 19 mpbid ⊢ Fun ⁡ A ∧ B ⊆ A ∧ x ∈ A ∧ ¬ x ∈ B ∧ 1 st ⁡ x = C → C ∈ dom ⁡ A ∖ dom ⁡ B
21 20 3exp ⊢ Fun ⁡ A ∧ B ⊆ A → x ∈ A ∧ ¬ x ∈ B → 1 st ⁡ x = C → C ∈ dom ⁡ A ∖ dom ⁡ B
22 4 21 syl5bi ⊢ Fun ⁡ A ∧ B ⊆ A → x ∈ A ∖ B → 1 st ⁡ x = C → C ∈ dom ⁡ A ∖ dom ⁡ B
23 22 rexlimdv ⊢ Fun ⁡ A ∧ B ⊆ A → ∃ x ∈ A ∖ B 1 st ⁡ x = C → C ∈ dom ⁡ A ∖ dom ⁡ B
24 3 23 impbid ⊢ Fun ⁡ A ∧ B ⊆ A → C ∈ dom ⁡ A ∖ dom ⁡ B ↔ ∃ x ∈ A ∖ B 1 st ⁡ x = C