| Step | Hyp | Ref
| Expression |
| 1 | | dirge.1 |
. . . . . . 7
⊢ 𝑋 = dom 𝑅 |
| 2 | | dirdm 18645 |
. . . . . . 7
⊢ (𝑅 ∈ DirRel → dom 𝑅 = ∪
∪ 𝑅) |
| 3 | 1, 2 | eqtrid 2789 |
. . . . . 6
⊢ (𝑅 ∈ DirRel → 𝑋 = ∪
∪ 𝑅) |
| 4 | 3 | eleq2d 2827 |
. . . . 5
⊢ (𝑅 ∈ DirRel → (𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ∪ ∪ 𝑅)) |
| 5 | 3 | eleq2d 2827 |
. . . . 5
⊢ (𝑅 ∈ DirRel → (𝐵 ∈ 𝑋 ↔ 𝐵 ∈ ∪ ∪ 𝑅)) |
| 6 | 4, 5 | anbi12d 632 |
. . . 4
⊢ (𝑅 ∈ DirRel → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ↔ (𝐴 ∈ ∪ ∪ 𝑅
∧ 𝐵 ∈ ∪ ∪ 𝑅))) |
| 7 | | eqid 2737 |
. . . . . . . . 9
⊢ ∪ ∪ 𝑅 = ∪ ∪ 𝑅 |
| 8 | 7 | isdir 18643 |
. . . . . . . 8
⊢ (𝑅 ∈ DirRel → (𝑅 ∈ DirRel ↔ ((Rel
𝑅 ∧ ( I ↾ ∪ ∪ 𝑅) ⊆ 𝑅) ∧ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (∪ ∪ 𝑅
× ∪ ∪ 𝑅) ⊆ (◡𝑅 ∘ 𝑅))))) |
| 9 | 8 | ibi 267 |
. . . . . . 7
⊢ (𝑅 ∈ DirRel → ((Rel
𝑅 ∧ ( I ↾ ∪ ∪ 𝑅) ⊆ 𝑅) ∧ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (∪ ∪ 𝑅
× ∪ ∪ 𝑅) ⊆ (◡𝑅 ∘ 𝑅)))) |
| 10 | 9 | simprrd 774 |
. . . . . 6
⊢ (𝑅 ∈ DirRel → (∪ ∪ 𝑅 × ∪ ∪ 𝑅)
⊆ (◡𝑅 ∘ 𝑅)) |
| 11 | | codir 6140 |
. . . . . 6
⊢ ((∪ ∪ 𝑅 × ∪ ∪ 𝑅)
⊆ (◡𝑅 ∘ 𝑅) ↔ ∀𝑦 ∈ ∪ ∪ 𝑅∀𝑧 ∈ ∪ ∪ 𝑅∃𝑥(𝑦𝑅𝑥 ∧ 𝑧𝑅𝑥)) |
| 12 | 10, 11 | sylib 218 |
. . . . 5
⊢ (𝑅 ∈ DirRel →
∀𝑦 ∈ ∪ ∪ 𝑅∀𝑧 ∈ ∪ ∪ 𝑅∃𝑥(𝑦𝑅𝑥 ∧ 𝑧𝑅𝑥)) |
| 13 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (𝑦𝑅𝑥 ↔ 𝐴𝑅𝑥)) |
| 14 | 13 | anbi1d 631 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ((𝑦𝑅𝑥 ∧ 𝑧𝑅𝑥) ↔ (𝐴𝑅𝑥 ∧ 𝑧𝑅𝑥))) |
| 15 | 14 | exbidv 1921 |
. . . . . 6
⊢ (𝑦 = 𝐴 → (∃𝑥(𝑦𝑅𝑥 ∧ 𝑧𝑅𝑥) ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑧𝑅𝑥))) |
| 16 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝑧𝑅𝑥 ↔ 𝐵𝑅𝑥)) |
| 17 | 16 | anbi2d 630 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → ((𝐴𝑅𝑥 ∧ 𝑧𝑅𝑥) ↔ (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 18 | 17 | exbidv 1921 |
. . . . . 6
⊢ (𝑧 = 𝐵 → (∃𝑥(𝐴𝑅𝑥 ∧ 𝑧𝑅𝑥) ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 19 | 15, 18 | rspc2v 3633 |
. . . . 5
⊢ ((𝐴 ∈ ∪ ∪ 𝑅 ∧ 𝐵 ∈ ∪ ∪ 𝑅)
→ (∀𝑦 ∈
∪ ∪ 𝑅∀𝑧 ∈ ∪ ∪ 𝑅∃𝑥(𝑦𝑅𝑥 ∧ 𝑧𝑅𝑥) → ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 20 | 12, 19 | syl5com 31 |
. . . 4
⊢ (𝑅 ∈ DirRel → ((𝐴 ∈ ∪ ∪ 𝑅 ∧ 𝐵 ∈ ∪ ∪ 𝑅)
→ ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 21 | 6, 20 | sylbid 240 |
. . 3
⊢ (𝑅 ∈ DirRel → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 22 | | reldir 18644 |
. . . . . . . . . 10
⊢ (𝑅 ∈ DirRel → Rel 𝑅) |
| 23 | | relelrn 5956 |
. . . . . . . . . 10
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝑥) → 𝑥 ∈ ran 𝑅) |
| 24 | 22, 23 | sylan 580 |
. . . . . . . . 9
⊢ ((𝑅 ∈ DirRel ∧ 𝐴𝑅𝑥) → 𝑥 ∈ ran 𝑅) |
| 25 | 24 | ex 412 |
. . . . . . . 8
⊢ (𝑅 ∈ DirRel → (𝐴𝑅𝑥 → 𝑥 ∈ ran 𝑅)) |
| 26 | | ssun2 4179 |
. . . . . . . . . . 11
⊢ ran 𝑅 ⊆ (dom 𝑅 ∪ ran 𝑅) |
| 27 | | dmrnssfld 5984 |
. . . . . . . . . . 11
⊢ (dom
𝑅 ∪ ran 𝑅) ⊆ ∪ ∪ 𝑅 |
| 28 | 26, 27 | sstri 3993 |
. . . . . . . . . 10
⊢ ran 𝑅 ⊆ ∪ ∪ 𝑅 |
| 29 | 28, 3 | sseqtrrid 4027 |
. . . . . . . . 9
⊢ (𝑅 ∈ DirRel → ran 𝑅 ⊆ 𝑋) |
| 30 | 29 | sseld 3982 |
. . . . . . . 8
⊢ (𝑅 ∈ DirRel → (𝑥 ∈ ran 𝑅 → 𝑥 ∈ 𝑋)) |
| 31 | 25, 30 | syld 47 |
. . . . . . 7
⊢ (𝑅 ∈ DirRel → (𝐴𝑅𝑥 → 𝑥 ∈ 𝑋)) |
| 32 | 31 | adantrd 491 |
. . . . . 6
⊢ (𝑅 ∈ DirRel → ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) → 𝑥 ∈ 𝑋)) |
| 33 | 32 | ancrd 551 |
. . . . 5
⊢ (𝑅 ∈ DirRel → ((𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) → (𝑥 ∈ 𝑋 ∧ (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))) |
| 34 | 33 | eximdv 1917 |
. . . 4
⊢ (𝑅 ∈ DirRel →
(∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) → ∃𝑥(𝑥 ∈ 𝑋 ∧ (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)))) |
| 35 | | df-rex 3071 |
. . . 4
⊢
(∃𝑥 ∈
𝑋 (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) ↔ ∃𝑥(𝑥 ∈ 𝑋 ∧ (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 36 | 34, 35 | imbitrrdi 252 |
. . 3
⊢ (𝑅 ∈ DirRel →
(∃𝑥(𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥) → ∃𝑥 ∈ 𝑋 (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 37 | 21, 36 | syld 47 |
. 2
⊢ (𝑅 ∈ DirRel → ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥))) |
| 38 | 37 | 3impib 1117 |
1
⊢ ((𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)) |