| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ersymb.1 | . . . . . . 7
⊢ (𝜑 → 𝑅 Er 𝑋) | 
| 2 |  | errel 8755 | . . . . . . 7
⊢ (𝑅 Er 𝑋 → Rel 𝑅) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝜑 → Rel 𝑅) | 
| 4 |  | simpr 484 | . . . . . 6
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐵𝑅𝐶) | 
| 5 |  | brrelex1 5737 | . . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐵 ∈ V) | 
| 6 | 3, 4, 5 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐵 ∈ V) | 
| 7 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) | 
| 8 |  | breq2 5146 | . . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) | 
| 9 |  | breq1 5145 | . . . . . 6
⊢ (𝑥 = 𝐵 → (𝑥𝑅𝐶 ↔ 𝐵𝑅𝐶)) | 
| 10 | 8, 9 | anbi12d 632 | . . . . 5
⊢ (𝑥 = 𝐵 → ((𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶))) | 
| 11 | 6, 7, 10 | spcedv 3597 | . . . 4
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶)) | 
| 12 |  | simpl 482 | . . . . . 6
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐵) | 
| 13 |  | brrelex1 5737 | . . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V) | 
| 14 | 3, 12, 13 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴 ∈ V) | 
| 15 |  | brrelex2 5738 | . . . . . 6
⊢ ((Rel
𝑅 ∧ 𝐵𝑅𝐶) → 𝐶 ∈ V) | 
| 16 | 3, 4, 15 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐶 ∈ V) | 
| 17 |  | brcog 5876 | . . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴(𝑅 ∘ 𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶))) | 
| 18 | 14, 16, 17 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → (𝐴(𝑅 ∘ 𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥𝑅𝐶))) | 
| 19 | 11, 18 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴(𝑅 ∘ 𝑅)𝐶) | 
| 20 | 19 | ex 412 | . 2
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴(𝑅 ∘ 𝑅)𝐶)) | 
| 21 |  | df-er 8746 | . . . . . 6
⊢ (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) | 
| 22 | 21 | simp3bi 1147 | . . . . 5
⊢ (𝑅 Er 𝑋 → (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) | 
| 23 | 1, 22 | syl 17 | . . . 4
⊢ (𝜑 → (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅) | 
| 24 | 23 | unssbd 4193 | . . 3
⊢ (𝜑 → (𝑅 ∘ 𝑅) ⊆ 𝑅) | 
| 25 | 24 | ssbrd 5185 | . 2
⊢ (𝜑 → (𝐴(𝑅 ∘ 𝑅)𝐶 → 𝐴𝑅𝐶)) | 
| 26 | 20, 25 | syld 47 | 1
⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |