Proof of Theorem vtoclr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vtoclr.1 | . . . . 5
⊢ Rel 𝑅 | 
| 2 | 1 | brrelex12i 5739 | . . . 4
⊢ (𝐴𝑅𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) | 
| 3 | 1 | brrelex2i 5741 | . . . 4
⊢ (𝐵𝑅𝐶 → 𝐶 ∈ V) | 
| 4 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥𝑅𝑦 ↔ 𝐴𝑅𝑦)) | 
| 5 | 4 | anbi1d 631 | . . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐶) ↔ (𝐴𝑅𝑦 ∧ 𝑦𝑅𝐶))) | 
| 6 |  | breq1 5145 | . . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥𝑅𝐶 ↔ 𝐴𝑅𝐶)) | 
| 7 | 5, 6 | imbi12d 344 | . . . . . 6
⊢ (𝑥 = 𝐴 → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝑥𝑅𝐶) ↔ ((𝐴𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝐴𝑅𝐶))) | 
| 8 | 7 | imbi2d 340 | . . . . 5
⊢ (𝑥 = 𝐴 → ((𝐶 ∈ V → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝑥𝑅𝐶)) ↔ (𝐶 ∈ V → ((𝐴𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝐴𝑅𝐶)))) | 
| 9 |  | breq2 5146 | . . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝐴𝑅𝑦 ↔ 𝐴𝑅𝐵)) | 
| 10 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝑦𝑅𝐶 ↔ 𝐵𝑅𝐶)) | 
| 11 | 9, 10 | anbi12d 632 | . . . . . . 7
⊢ (𝑦 = 𝐵 → ((𝐴𝑅𝑦 ∧ 𝑦𝑅𝐶) ↔ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶))) | 
| 12 | 11 | imbi1d 341 | . . . . . 6
⊢ (𝑦 = 𝐵 → (((𝐴𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝐴𝑅𝐶) ↔ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) | 
| 13 | 12 | imbi2d 340 | . . . . 5
⊢ (𝑦 = 𝐵 → ((𝐶 ∈ V → ((𝐴𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝐴𝑅𝐶)) ↔ (𝐶 ∈ V → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)))) | 
| 14 |  | breq2 5146 | . . . . . . . 8
⊢ (𝑧 = 𝐶 → (𝑦𝑅𝑧 ↔ 𝑦𝑅𝐶)) | 
| 15 | 14 | anbi2d 630 | . . . . . . 7
⊢ (𝑧 = 𝐶 → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ↔ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝐶))) | 
| 16 |  | breq2 5146 | . . . . . . 7
⊢ (𝑧 = 𝐶 → (𝑥𝑅𝑧 ↔ 𝑥𝑅𝐶)) | 
| 17 | 15, 16 | imbi12d 344 | . . . . . 6
⊢ (𝑧 = 𝐶 → (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝑥𝑅𝐶))) | 
| 18 |  | vtoclr.2 | . . . . . 6
⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) | 
| 19 | 17, 18 | vtoclg 3553 | . . . . 5
⊢ (𝐶 ∈ V → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝐶) → 𝑥𝑅𝐶)) | 
| 20 | 8, 13, 19 | vtocl2g 3573 | . . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐶 ∈ V → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) | 
| 21 | 2, 3, 20 | syl2im 40 | . . 3
⊢ (𝐴𝑅𝐵 → (𝐵𝑅𝐶 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))) | 
| 22 | 21 | imp 406 | . 2
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) | 
| 23 | 22 | pm2.43i 52 | 1
⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) |