Metamath Proof Explorer

Theorem vtoclr

Description: Variable to class conversion of transitive relation. (Contributed by NM, 9-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses vtoclr.1 ⊢ Rel 𝑅
vtoclr.2 ⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 )
Assertion vtoclr ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 )

Proof

Step Hyp Ref Expression
1 vtoclr.1 ⊢ Rel 𝑅
2 vtoclr.2 ⊢ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 )
3 1 brrelex12i ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
4 1 brrelex2i ⊢ ( 𝐵 𝑅 𝐶 → 𝐶 ∈ V )
5 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑦 ↔ 𝐴 𝑅 𝑦 ) )
6 5 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) ↔ ( 𝐴 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) ) )
7 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝐶 ↔ 𝐴 𝑅 𝐶 ) )
8 6 7 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝑥 𝑅 𝐶 ) ↔ ( ( 𝐴 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐶 ∈ V → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝑥 𝑅 𝐶 ) ) ↔ ( 𝐶 ∈ V → ( ( 𝐴 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) ) )
10 breq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝑅 𝑦 ↔ 𝐴 𝑅 𝐵 ) )
11 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) )
12 10 11 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) )
13 12 imbi1d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝐴 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ↔ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
14 13 imbi2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐶 ∈ V → ( ( 𝐴 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) ↔ ( 𝐶 ∈ V → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) ) )
15 breq2 ⊢ ( 𝑧 = 𝐶 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑅 𝐶 ) )
16 15 anbi2d ⊢ ( 𝑧 = 𝐶 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) ) )
17 breq2 ⊢ ( 𝑧 = 𝐶 → ( 𝑥 𝑅 𝑧 ↔ 𝑥 𝑅 𝐶 ) )
18 16 17 imbi12d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝑥 𝑅 𝐶 ) ) )
19 18 2 vtoclg ⊢ ( 𝐶 ∈ V → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝐶 ) → 𝑥 𝑅 𝐶 ) )
20 9 14 19 vtocl2g ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐶 ∈ V → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
21 3 4 20 syl2im ⊢ ( 𝐴 𝑅 𝐵 → ( 𝐵 𝑅 𝐶 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) )
22 21 imp ⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) )
23 22 pm2.43i ⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 )