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 𝐴 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐶 ∈ ( dom 𝐴 ∖ dom 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ( 1st ‘ 𝑥 ) = 𝐶 ) )

Proof

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