Proof of Theorem releldmdifi
| Step | Hyp | Ref
| Expression |
| 1 | | eldif 3961 |
. . 3
⊢ (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) ↔ (𝐶 ∈ dom 𝐴 ∧ ¬ 𝐶 ∈ dom 𝐵)) |
| 2 | | releldm2 8068 |
. . . . 5
⊢ (Rel
𝐴 → (𝐶 ∈ dom 𝐴 ↔ ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶)) |
| 3 | 2 | adantr 480 |
. . . 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 771 |
. . . 4
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶) |
| 7 | | relss 5791 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ 𝐴 → (Rel 𝐴 → Rel 𝐵)) |
| 8 | 7 | impcom 407 |
. . . . . . . . . . 11
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → Rel 𝐵) |
| 9 | | 1stdm 8065 |
. . . . . . . . . . 11
⊢ ((Rel
𝐵 ∧ 𝑥 ∈ 𝐵) → (1st ‘𝑥) ∈ dom 𝐵) |
| 10 | 8, 9 | sylan 580 |
. . . . . . . . . 10
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝐵) → (1st ‘𝑥) ∈ dom 𝐵) |
| 11 | | eleq1 2829 |
. . . . . . . . . 10
⊢
((1st ‘𝑥) = 𝐶 → ((1st ‘𝑥) ∈ dom 𝐵 ↔ 𝐶 ∈ dom 𝐵)) |
| 12 | 10, 11 | syl5ibcom 245 |
. . . . . . . . 9
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ 𝑥 ∈ 𝐵) → ((1st ‘𝑥) = 𝐶 → 𝐶 ∈ dom 𝐵)) |
| 13 | 12 | rexlimdva 3155 |
. . . . . . . 8
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶 → 𝐶 ∈ dom 𝐵)) |
| 14 | 13 | con3d 152 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (¬ 𝐶 ∈ dom 𝐵 → ¬ ∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶)) |
| 15 | | ralnex 3072 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ¬ (1st
‘𝑥) = 𝐶 ↔ ¬ ∃𝑥 ∈ 𝐵 (1st ‘𝑥) = 𝐶) |
| 16 | 14, 15 | imbitrrdi 252 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (¬ 𝐶 ∈ dom 𝐵 → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶)) |
| 17 | 16 | adantld 490 |
. . . . 5
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵) → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶)) |
| 18 | 17 | imp 406 |
. . . 4
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶) |
| 19 | | rexdifi 4150 |
. . . 4
⊢
((∃𝑥 ∈
𝐴 (1st
‘𝑥) = 𝐶 ∧ ∀𝑥 ∈ 𝐵 ¬ (1st ‘𝑥) = 𝐶) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶) |
| 20 | 6, 18, 19 | syl2anc 584 |
. . 3
⊢ (((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) ∧ (∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵)) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶) |
| 21 | 20 | ex 412 |
. 2
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → ((∃𝑥 ∈ 𝐴 (1st ‘𝑥) = 𝐶 ∧ ¬ 𝐶 ∈ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) |
| 22 | 5, 21 | sylbid 240 |
1
⊢ ((Rel
𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝐶 ∈ (dom 𝐴 ∖ dom 𝐵) → ∃𝑥 ∈ (𝐴 ∖ 𝐵)(1st ‘𝑥) = 𝐶)) |