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 syl5bb ( ( 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 syl6ibr ( ( 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𝑥 ) = 𝐶 ) )