Step | Hyp | Ref
| Expression |
1 | | ersymb.1 |
. . . . . . 7
⊢ (𝜑 → 𝑅 Er 𝑋) |
2 | | errel 6491 |
. . . . . . 7
⊢ (𝑅 Er 𝑋 → Rel 𝑅) |
3 | 1, 2 | syl 14 |
. . . . . 6
⊢ (𝜑 → Rel 𝑅) |
4 | | simpr 109 |
. . . . . 6
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐵𝑅𝐶) |
5 | | brrelex 4628 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐵 ∈ V) |
6 | 3, 4, 5 | syl2an 287 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐵 ∈ V) |
7 | | simpr 109 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) |
8 | | breq2 3971 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) |
9 | | breq1 3970 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝑥𝑅𝐶 ↔ 𝐵𝑅𝐶)) |
10 | 8, 9 | anbi12d 465 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ((𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶))) |
11 | 10 | spcegv 2800 |
. . . . 5
⊢ (𝐵 ∈ V → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶))) |
12 | 6, 7, 11 | sylc 62 |
. . . 4
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶)) |
13 | | simpl 108 |
. . . . . 6
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐵) |
14 | | brrelex 4628 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) |
15 | 3, 13, 14 | syl2an 287 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴 ∈ V) |
16 | | brrelex2 4629 |
. . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐶 ∈ V) |
17 | 3, 4, 16 | syl2an 287 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐶 ∈ V) |
18 | | brcog 4755 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴(𝑅 ∘ 𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶))) |
19 | 15, 17, 18 | syl2anc 409 |
. . . 4
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → (𝐴(𝑅 ∘ 𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶))) |
20 | 12, 19 | mpbird 166 |
. . 3
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴(𝑅 ∘ 𝑅)𝐶) |
21 | 20 | ex 114 |
. 2
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴(𝑅 ∘ 𝑅)𝐶)) |
22 | | df-er 6482 |
. . . . . 6
⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) |
23 | 22 | simp3bi 999 |
. . . . 5
⊢ (𝑅 Er 𝑋 → (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) |
24 | 1, 23 | syl 14 |
. . . 4
⊢ (𝜑 → (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) |
25 | 24 | unssbd 3286 |
. . 3
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) |
26 | 25 | ssbrd 4009 |
. 2
⊢ (𝜑 → (𝐴(𝑅 ∘ 𝑅)𝐶 → 𝐴𝑅𝐶)) |
27 | 21, 26 | syld 45 |
1
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |