Step | Hyp | Ref
| Expression |
1 | | ersymb.1 |
. . . . . . 7
⊢ (𝜑 → 𝑅 Er 𝑋) |
2 | | errel 8465 |
. . . . . . 7
⊢ (𝑅 Er 𝑋 → Rel 𝑅) |
3 | 1, 2 | syl 17 |
. . . . . 6
⊢ (𝜑 → Rel 𝑅) |
4 | | simpr 484 |
. . . . . 6
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐵𝑅𝐶) |
5 | | brrelex1 5631 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐵 ∈ V) |
6 | 3, 4, 5 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐵 ∈ V) |
7 | | simpr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) |
8 | | breq2 5074 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) |
9 | | breq1 5073 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝑥𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
10 | 8, 9 | anbi12d 630 |
. . . . 5
⊢ (𝑥 = 𝐵 → ((𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶))) |
11 | 6, 7, 10 | spcedv 3527 |
. . . 4
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶)) |
12 | | simpl 482 |
. . . . . 6
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐵) |
13 | | brrelex1 5631 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) |
14 | 3, 12, 13 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴 ∈ V) |
15 | | brrelex2 5632 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐶 ∈ V) |
16 | 3, 4, 15 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐶 ∈ V) |
17 | | brcog 5764 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴(𝑅 ∘ 𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶))) |
18 | 14, 16, 17 | syl2anc 583 |
. . . 4
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → (𝐴(𝑅 ∘ 𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶))) |
19 | 11, 18 | mpbird 256 |
. . 3
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴(𝑅 ∘ 𝑅)𝐶) |
20 | 19 | ex 412 |
. 2
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴(𝑅 ∘ 𝑅)𝐶)) |
21 | | df-er 8456 |
. . . . . 6
⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) |
22 | 21 | simp3bi 1145 |
. . . . 5
⊢ (𝑅 Er 𝑋 → (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) |
23 | 1, 22 | syl 17 |
. . . 4
⊢ (𝜑 → (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) |
24 | 23 | unssbd 4118 |
. . 3
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) |
25 | 24 | ssbrd 5113 |
. 2
⊢ (𝜑 → (𝐴(𝑅 ∘ 𝑅)𝐶 → 𝐴𝑅𝐶)) |
26 | 20, 25 | syld 47 |
1
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |