Step | Hyp | Ref
| Expression |
1 | | eldif 3921 |
. . 3
⊢ (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) ↔ (𝐶 ∈ dom 𝐴 ∧ ¬ 𝐶 ∈ dom 𝐵)) |
2 | | releldm2 7976 |
. . . . 5
⊢ (Rel
𝐴 → (𝐶 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶)) |
3 | 2 | adantr 482 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶)) |
4 | 3 | anbi1d 631 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∈ dom 𝐴 ∧ ¬ 𝐶 ∈ dom 𝐵) ↔ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵))) |
5 | 1, 4 | bitrid 283 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) ↔ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵))) |
6 | | simprl 770 |
. . . 4
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶) |
7 | | relss 5738 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ 𝐴 → (Rel 𝐴 → Rel 𝐵)) |
8 | 7 | impcom 409 |
. . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → Rel 𝐵) |
9 | | 1stdm 7973 |
. . . . . . . . . . 11
⊢ ((Rel
𝐵 ∧ 𝑥 ∈ 𝐵) → (1st ‘𝑥) ∈ dom 𝐵) |
10 | 8, 9 | sylan 581 |
. . . . . . . . . 10
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝐵) → (1st ‘𝑥) ∈ dom 𝐵) |
11 | | eleq1 2826 |
. . . . . . . . . 10
⊢
((1st ‘𝑥) = 𝐶 → ((1st ‘𝑥) ∈ dom 𝐵 ↔ 𝐶 ∈ dom 𝐵)) |
12 | 10, 11 | syl5ibcom 244 |
. . . . . . . . 9
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((1st ‘𝑥) = 𝐶 → 𝐶 ∈ dom 𝐵)) |
13 | 12 | rexlimdva 3153 |
. . . . . . . 8
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶 → 𝐶 ∈ dom 𝐵)) |
14 | 13 | con3d 152 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (¬ 𝐶 ∈ dom 𝐵 → ¬ ∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶)) |
15 | | ralnex 3076 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ¬ (1st
‘𝑥) = 𝐶 ↔ ¬ ∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶) |
16 | 14, 15 | syl6ibr 252 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (¬ 𝐶 ∈ dom 𝐵 → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶)) |
17 | 16 | adantld 492 |
. . . . 5
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵) → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶)) |
18 | 17 | imp 408 |
. . . 4
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶) |
19 | | rexdifi 4106 |
. . . 4
⊢
((∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐶 ∧ ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶) |
20 | 6, 18, 19 | syl2anc 585 |
. . 3
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶) |
21 | 20 | ex 414 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) |
22 | 5, 21 | sylbid 239 |
1
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) |