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∖B1st⁡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∈A1st⁡x=C
3 2 adantr ⊢Rel⁡A∧B⊆A→C∈dom⁡A↔∃x∈A1st⁡x=C
4 3 anbi1d ⊢Rel⁡A∧B⊆A→C∈dom⁡A∧¬C∈dom⁡B↔∃x∈A1st⁡x=C∧¬C∈dom⁡B
5 1 4 bitrid ⊢Rel⁡A∧B⊆A→C∈dom⁡A∖dom⁡B↔∃x∈A1st⁡x=C∧¬C∈dom⁡B
6 simprl ⊢Rel⁡A∧B⊆A∧∃x∈A1st⁡x=C∧¬C∈dom⁡B→∃x∈A1st⁡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→1st⁡x∈dom⁡B
10 8 9 sylan ⊢Rel⁡A∧B⊆A∧x∈B→1st⁡x∈dom⁡B
11 eleq1 ⊢1st⁡x=C→1st⁡x∈dom⁡B↔C∈dom⁡B
12 10 11 syl5ibcom ⊢Rel⁡A∧B⊆A∧x∈B→1st⁡x=C→C∈dom⁡B
13 12 rexlimdva ⊢Rel⁡A∧B⊆A→∃x∈B1st⁡x=C→C∈dom⁡B
14 13 con3d ⊢Rel⁡A∧B⊆A→¬C∈dom⁡B→¬∃x∈B1st⁡x=C
15 ralnex ⊢∀x∈B¬1st⁡x=C↔¬∃x∈B1st⁡x=C
16 14 15 imbitrrdi ⊢Rel⁡A∧B⊆A→¬C∈dom⁡B→∀x∈B¬1st⁡x=C
17 16 adantld ⊢Rel⁡A∧B⊆A→∃x∈A1st⁡x=C∧¬C∈dom⁡B→∀x∈B¬1st⁡x=C
18 17 imp ⊢Rel⁡A∧B⊆A∧∃x∈A1st⁡x=C∧¬C∈dom⁡B→∀x∈B¬1st⁡x=C
19 rexdifi ⊢∃x∈A1st⁡x=C∧∀x∈B¬1st⁡x=C→∃x∈A∖B1st⁡x=C
20 6 18 19 syl2anc ⊢Rel⁡A∧B⊆A∧∃x∈A1st⁡x=C∧¬C∈dom⁡B→∃x∈A∖B1st⁡x=C
21 20 ex ⊢Rel⁡A∧B⊆A→∃x∈A1st⁡x=C∧¬C∈dom⁡B→∃x∈A∖B1st⁡x=C
22 5 21 sylbid ⊢Rel⁡A∧B⊆A→C∈dom⁡A∖dom⁡B→∃x∈A∖B1st⁡x=C