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 ‘ 𝑥 ) = 𝐶 ) ) |