Proof of Theorem releldmdifi
Step | Hyp | Ref
| Expression |
1 | | eldif 3876 |
. . 3
⊢ (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) ↔ (𝐶 ∈ dom 𝐴 ∧ ¬ 𝐶 ∈ dom 𝐵)) |
2 | | releldm2 7814 |
. . . . 5
⊢ (Rel
𝐴 → (𝐶 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶)) |
3 | 2 | adantr 484 |
. . . 4
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶)) |
4 | 3 | anbi1d 633 |
. . 3
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ∈ dom 𝐴 ∧ ¬ 𝐶 ∈ dom 𝐵) ↔ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵))) |
5 | 1, 4 | syl5bb 286 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) ↔ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵))) |
6 | | simprl 771 |
. . . 4
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶) |
7 | | relss 5653 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ 𝐴 → (Rel 𝐴 → Rel 𝐵)) |
8 | 7 | impcom 411 |
. . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → Rel 𝐵) |
9 | | 1stdm 7811 |
. . . . . . . . . . 11
⊢ ((Rel
𝐵 ∧ 𝑥 ∈ 𝐵) → (1st ‘𝑥) ∈ dom 𝐵) |
10 | 8, 9 | sylan 583 |
. . . . . . . . . 10
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝐵) → (1st ‘𝑥) ∈ dom 𝐵) |
11 | | eleq1 2825 |
. . . . . . . . . 10
⊢
((1st ‘𝑥) = 𝐶 → ((1st ‘𝑥) ∈ dom 𝐵 ↔ 𝐶 ∈ dom 𝐵)) |
12 | 10, 11 | syl5ibcom 248 |
. . . . . . . . 9
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((1st ‘𝑥) = 𝐶 → 𝐶 ∈ dom 𝐵)) |
13 | 12 | rexlimdva 3203 |
. . . . . . . 8
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶 → 𝐶 ∈ dom 𝐵)) |
14 | 13 | con3d 155 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (¬ 𝐶 ∈ dom 𝐵 → ¬ ∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶)) |
15 | | ralnex 3158 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ¬ (1st
‘𝑥) = 𝐶 ↔ ¬ ∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶) |
16 | 14, 15 | syl6ibr 255 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (¬ 𝐶 ∈ dom 𝐵 → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶)) |
17 | 16 | adantld 494 |
. . . . 5
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵) → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶)) |
18 | 17 | imp 410 |
. . . 4
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶) |
19 | | rexdifi 4060 |
. . . 4
⊢
((∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐶 ∧ ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶) |
20 | 6, 18, 19 | syl2anc 587 |
. . 3
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶) |
21 | 20 | ex 416 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) |
22 | 5, 21 | sylbid 243 |
1
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) |