Step |
Hyp |
Ref |
Expression |
1 |
|
eqvreltr.1 |
⊢ ( 𝜑 → EqvRel 𝑅 ) |
2 |
|
eqvrelrel |
⊢ ( EqvRel 𝑅 → Rel 𝑅 ) |
3 |
1 2
|
syl |
⊢ ( 𝜑 → Rel 𝑅 ) |
4 |
|
simpr |
⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐵 𝑅 𝐶 ) |
5 |
|
brrelex1 |
⊢ ( ( Rel 𝑅 ∧ 𝐵 𝑅 𝐶 ) → 𝐵 ∈ V ) |
6 |
3 4 5
|
syl2an |
⊢ ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → 𝐵 ∈ V ) |
7 |
|
simpr |
⊢ ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) |
8 |
|
breq2 |
⊢ ( 𝑥 = 𝐵 → ( 𝐴 𝑅 𝑥 ↔ 𝐴 𝑅 𝐵 ) ) |
9 |
|
breq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) ) |
10 |
8 9
|
anbi12d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 𝑅 𝑥 ∧ 𝑥 𝑅 𝐶 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) ) |
11 |
6 7 10
|
spcedv |
⊢ ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝑥 𝑅 𝐶 ) ) |
12 |
|
simpl |
⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐵 ) |
13 |
|
brrelex1 |
⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝐵 ) → 𝐴 ∈ V ) |
14 |
3 12 13
|
syl2an |
⊢ ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → 𝐴 ∈ V ) |
15 |
|
brrelex2 |
⊢ ( ( Rel 𝑅 ∧ 𝐵 𝑅 𝐶 ) → 𝐶 ∈ V ) |
16 |
3 4 15
|
syl2an |
⊢ ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → 𝐶 ∈ V ) |
17 |
|
brcog |
⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ( 𝑅 ∘ 𝑅 ) 𝐶 ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝑥 𝑅 𝐶 ) ) ) |
18 |
14 16 17
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → ( 𝐴 ( 𝑅 ∘ 𝑅 ) 𝐶 ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝑥 𝑅 𝐶 ) ) ) |
19 |
11 18
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) ) → 𝐴 ( 𝑅 ∘ 𝑅 ) 𝐶 ) |
20 |
19
|
ex |
⊢ ( 𝜑 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 ( 𝑅 ∘ 𝑅 ) 𝐶 ) ) |
21 |
|
dfeqvrel2 |
⊢ ( EqvRel 𝑅 ↔ ( ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ∧ Rel 𝑅 ) ) |
22 |
21
|
simplbi |
⊢ ( EqvRel 𝑅 → ( ( I ↾ dom 𝑅 ) ⊆ 𝑅 ∧ ◡ 𝑅 ⊆ 𝑅 ∧ ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) ) |
23 |
22
|
simp3d |
⊢ ( EqvRel 𝑅 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) |
24 |
1 23
|
syl |
⊢ ( 𝜑 → ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ) |
25 |
24
|
ssbrd |
⊢ ( 𝜑 → ( 𝐴 ( 𝑅 ∘ 𝑅 ) 𝐶 → 𝐴 𝑅 𝐶 ) ) |
26 |
20 25
|
syld |
⊢ ( 𝜑 → ( ( 𝐴 𝑅 𝐵 ∧ 𝐵 𝑅 𝐶 ) → 𝐴 𝑅 𝐶 ) ) |