Metamath Proof Explorer

Theorem releldmdifi

Description: One way of expressing membership in the difference of domains of two nested relations. (Contributed by AV, 26-Oct-2023)

Ref Expression
Assertion releldmdifi ⊢ Rel ⁡ A ∧ B ⊆ A → C ∈ dom ⁡ A ∖ dom ⁡ B → ∃ x ∈ A ∖ B 1 st ⁡ x = C

Proof

Step Hyp Ref Expression
1 eldif ⊢ C ∈ dom ⁡ A ∖ dom ⁡ B ↔ C ∈ dom ⁡ A ∧ ¬ C ∈ dom ⁡ B
2 releldm2 ⊢ Rel ⁡ A → C ∈ dom ⁡ A ↔ ∃ x ∈ A 1 st ⁡ x = C
3 2 adantr ⊢ Rel ⁡ A ∧ B ⊆ A → C ∈ dom ⁡ A ↔ ∃ x ∈ A 1 st ⁡ x = C
4 3 anbi1d ⊢ Rel ⁡ A ∧ B ⊆ A → C ∈ dom ⁡ A ∧ ¬ C ∈ dom ⁡ B ↔ ∃ x ∈ A 1 st ⁡ x = C ∧ ¬ C ∈ dom ⁡ B
5 1 4 bitrid ⊢ Rel ⁡ A ∧ B ⊆ A → C ∈ dom ⁡ A ∖ dom ⁡ B ↔ ∃ x ∈ A 1 st ⁡ x = C ∧ ¬ C ∈ dom ⁡ B
6 simprl ⊢ Rel ⁡ A ∧ B ⊆ A ∧ ∃ x ∈ A 1 st ⁡ x = C ∧ ¬ C ∈ dom ⁡ B → ∃ x ∈ A 1 st ⁡ x = C
7 relss ⊢ B ⊆ A → Rel ⁡ A → Rel ⁡ B
8 7 impcom ⊢ Rel ⁡ A ∧ B ⊆ A → Rel ⁡ B
9 1stdm ⊢ Rel ⁡ B ∧ x ∈ B → 1 st ⁡ x ∈ dom ⁡ B
10 8 9 sylan ⊢ Rel ⁡ A ∧ B ⊆ A ∧ x ∈ B → 1 st ⁡ x ∈ dom ⁡ B
11 eleq1 ⊢ 1 st ⁡ x = C → 1 st ⁡ x ∈ dom ⁡ B ↔ C ∈ dom ⁡ B
12 10 11 syl5ibcom ⊢ Rel ⁡ A ∧ B ⊆ A ∧ x ∈ B → 1 st ⁡ x = C → C ∈ dom ⁡ B
13 12 rexlimdva ⊢ Rel ⁡ A ∧ B ⊆ A → ∃ x ∈ B 1 st ⁡ x = C → C ∈ dom ⁡ B
14 13 con3d ⊢ Rel ⁡ A ∧ B ⊆ A → ¬ C ∈ dom ⁡ B → ¬ ∃ x ∈ B 1 st ⁡ x = C
15 ralnex ⊢ ∀ x ∈ B ¬ 1 st ⁡ x = C ↔ ¬ ∃ x ∈ B 1 st ⁡ x = C
16 14 15 imbitrrdi ⊢ Rel ⁡ A ∧ B ⊆ A → ¬ C ∈ dom ⁡ B → ∀ x ∈ B ¬ 1 st ⁡ x = C
17 16 adantld ⊢ Rel ⁡ A ∧ B ⊆ A → ∃ x ∈ A 1 st ⁡ x = C ∧ ¬ C ∈ dom ⁡ B → ∀ x ∈ B ¬ 1 st ⁡ x = C
18 17 imp ⊢ Rel ⁡ A ∧ B ⊆ A ∧ ∃ x ∈ A 1 st ⁡ x = C ∧ ¬ C ∈ dom ⁡ B → ∀ x ∈ B ¬ 1 st ⁡ x = C
19 rexdifi ⊢ ∃ x ∈ A 1 st ⁡ x = C ∧ ∀ x ∈ B ¬ 1 st ⁡ x = C → ∃ x ∈ A ∖ B 1 st ⁡ x = C
20 6 18 19 syl2anc ⊢ Rel ⁡ A ∧ B ⊆ A ∧ ∃ x ∈ A 1 st ⁡ x = C ∧ ¬ C ∈ dom ⁡ B → ∃ x ∈ A ∖ B 1 st ⁡ x = C
21 20 ex ⊢ Rel ⁡ A ∧ B ⊆ A → ∃ x ∈ A 1 st ⁡ x = C ∧ ¬ C ∈ dom ⁡ B → ∃ x ∈ A ∖ B 1 st ⁡ x = C
22 5 21 sylbid ⊢ Rel ⁡ A ∧ B ⊆ A → C ∈ dom ⁡ A ∖ dom ⁡ B → ∃ x ∈ A ∖ B 1 st ⁡ x = C