Step | Hyp | Ref
| Expression |
1 | | relxp 5655 |
. . . . . . . . 9
⊢ Rel
(𝐴 × 𝐴) |
2 | | relss 5741 |
. . . . . . . . 9
⊢ (𝑅 ⊆ (𝐴 × 𝐴) → (Rel (𝐴 × 𝐴) → Rel 𝑅)) |
3 | 1, 2 | mpi 20 |
. . . . . . . 8
⊢ (𝑅 ⊆ (𝐴 × 𝐴) → Rel 𝑅) |
4 | 3 | ad2antlr 726 |
. . . . . . 7
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ ¬ 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅)) → Rel 𝑅) |
5 | | df-br 5110 |
. . . . . . . . . 10
⊢ (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅) |
6 | | ssun1 4136 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑥}) |
7 | | undif1 4439 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∖ {𝑥}) ∪ {𝑥}) = (𝐴 ∪ {𝑥}) |
8 | 6, 7 | sseqtrri 3985 |
. . . . . . . . . . . 12
⊢ 𝐴 ⊆ ((𝐴 ∖ {𝑥}) ∪ {𝑥}) |
9 | | simpll 766 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → 𝑅 Or 𝐴) |
10 | | dmss 5862 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 ⊆ (𝐴 × 𝐴) → dom 𝑅 ⊆ dom (𝐴 × 𝐴)) |
11 | | dmxpid 5889 |
. . . . . . . . . . . . . . . . 17
⊢ dom
(𝐴 × 𝐴) = 𝐴 |
12 | 10, 11 | sseqtrdi 3998 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ⊆ (𝐴 × 𝐴) → dom 𝑅 ⊆ 𝐴) |
13 | 12 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → dom 𝑅 ⊆ 𝐴) |
14 | 3 | ad2antlr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → Rel 𝑅) |
15 | | releldm 5903 |
. . . . . . . . . . . . . . . 16
⊢ ((Rel
𝑅 ∧ 𝑥𝑅𝑦) → 𝑥 ∈ dom 𝑅) |
16 | 14, 15 | sylancom 589 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → 𝑥 ∈ dom 𝑅) |
17 | 13, 16 | sseldd 3949 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → 𝑥 ∈ 𝐴) |
18 | | sossfld 6142 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∖ {𝑥}) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
19 | 9, 17, 18 | syl2anc 585 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → (𝐴 ∖ {𝑥}) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
20 | | ssun1 4136 |
. . . . . . . . . . . . . . 15
⊢ dom 𝑅 ⊆ (dom 𝑅 ∪ ran 𝑅) |
21 | 20, 16 | sselid 3946 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → 𝑥 ∈ (dom 𝑅 ∪ ran 𝑅)) |
22 | 21 | snssd 4773 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → {𝑥} ⊆ (dom 𝑅 ∪ ran 𝑅)) |
23 | 19, 22 | unssd 4150 |
. . . . . . . . . . . 12
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → ((𝐴 ∖ {𝑥}) ∪ {𝑥}) ⊆ (dom 𝑅 ∪ ran 𝑅)) |
24 | 8, 23 | sstrid 3959 |
. . . . . . . . . . 11
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ 𝑥𝑅𝑦) → 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅)) |
25 | 24 | ex 414 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) → (𝑥𝑅𝑦 → 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅))) |
26 | 5, 25 | biimtrrid 242 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) → (⟨𝑥, 𝑦⟩ ∈ 𝑅 → 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅))) |
27 | 26 | con3dimp 410 |
. . . . . . . 8
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ ¬ 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅)) → ¬ ⟨𝑥, 𝑦⟩ ∈ 𝑅) |
28 | 27 | pm2.21d 121 |
. . . . . . 7
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ ¬ 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅)) → (⟨𝑥, 𝑦⟩ ∈ 𝑅 → ⟨𝑥, 𝑦⟩ ∈ ∅)) |
29 | 4, 28 | relssdv 5748 |
. . . . . 6
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ ¬ 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅)) → 𝑅 ⊆ ∅) |
30 | | ss0 4362 |
. . . . . 6
⊢ (𝑅 ⊆ ∅ → 𝑅 = ∅) |
31 | 29, 30 | syl 17 |
. . . . 5
⊢ (((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) ∧ ¬ 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅)) → 𝑅 = ∅) |
32 | 31 | ex 414 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) → (¬ 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅) → 𝑅 = ∅)) |
33 | 32 | necon1ad 2957 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴)) → (𝑅 ≠ ∅ → 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅))) |
34 | 33 | 3impia 1118 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴) ∧ 𝑅 ≠ ∅) → 𝐴 ⊆ (dom 𝑅 ∪ ran 𝑅)) |
35 | | rnss 5898 |
. . . . 5
⊢ (𝑅 ⊆ (𝐴 × 𝐴) → ran 𝑅 ⊆ ran (𝐴 × 𝐴)) |
36 | | rnxpid 6129 |
. . . . 5
⊢ ran
(𝐴 × 𝐴) = 𝐴 |
37 | 35, 36 | sseqtrdi 3998 |
. . . 4
⊢ (𝑅 ⊆ (𝐴 × 𝐴) → ran 𝑅 ⊆ 𝐴) |
38 | 12, 37 | unssd 4150 |
. . 3
⊢ (𝑅 ⊆ (𝐴 × 𝐴) → (dom 𝑅 ∪ ran 𝑅) ⊆ 𝐴) |
39 | 38 | 3ad2ant2 1135 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴) ∧ 𝑅 ≠ ∅) → (dom 𝑅 ∪ ran 𝑅) ⊆ 𝐴) |
40 | 34, 39 | eqssd 3965 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝑅 ⊆ (𝐴 × 𝐴) ∧ 𝑅 ≠ ∅) → 𝐴 = (dom 𝑅 ∪ ran 𝑅)) |