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

Proof

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