Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
RP ADDTO: The reflexive and transitive properties of relations
cnvssco
Next ⟩
refimssco
Metamath Proof Explorer
Ascii
Unicode
Theorem
cnvssco
Description:
A condition weaker than reflexivity.
(Contributed by
RP
, 3-Aug-2020)
Ref
Expression
Assertion
cnvssco
⊢
A
-1
⊆
B
∘
C
-1
↔
∀
x
∀
y
∃
z
x
A
y
→
x
C
z
∧
z
B
y
Proof
Step
Hyp
Ref
Expression
1
alcom
⊢
∀
y
∀
x
y
x
∈
A
-1
→
y
x
∈
B
∘
C
-1
↔
∀
x
∀
y
y
x
∈
A
-1
→
y
x
∈
B
∘
C
-1
2
relcnv
⊢
Rel
⁡
A
-1
3
ssrel
⊢
Rel
⁡
A
-1
→
A
-1
⊆
B
∘
C
-1
↔
∀
y
∀
x
y
x
∈
A
-1
→
y
x
∈
B
∘
C
-1
4
2
3
ax-mp
⊢
A
-1
⊆
B
∘
C
-1
↔
∀
y
∀
x
y
x
∈
A
-1
→
y
x
∈
B
∘
C
-1
5
19.37v
⊢
∃
z
x
A
y
→
x
C
z
∧
z
B
y
↔
x
A
y
→
∃
z
x
C
z
∧
z
B
y
6
vex
⊢
y
∈
V
7
vex
⊢
x
∈
V
8
6
7
brcnv
⊢
y
A
-1
x
↔
x
A
y
9
df-br
⊢
y
A
-1
x
↔
y
x
∈
A
-1
10
8
9
bitr3i
⊢
x
A
y
↔
y
x
∈
A
-1
11
7
6
brco
⊢
x
B
∘
C
y
↔
∃
z
x
C
z
∧
z
B
y
12
6
7
brcnv
⊢
y
B
∘
C
-1
x
↔
x
B
∘
C
y
13
df-br
⊢
y
B
∘
C
-1
x
↔
y
x
∈
B
∘
C
-1
14
12
13
bitr3i
⊢
x
B
∘
C
y
↔
y
x
∈
B
∘
C
-1
15
11
14
bitr3i
⊢
∃
z
x
C
z
∧
z
B
y
↔
y
x
∈
B
∘
C
-1
16
10
15
imbi12i
⊢
x
A
y
→
∃
z
x
C
z
∧
z
B
y
↔
y
x
∈
A
-1
→
y
x
∈
B
∘
C
-1
17
5
16
bitri
⊢
∃
z
x
A
y
→
x
C
z
∧
z
B
y
↔
y
x
∈
A
-1
→
y
x
∈
B
∘
C
-1
18
17
2albii
⊢
∀
x
∀
y
∃
z
x
A
y
→
x
C
z
∧
z
B
y
↔
∀
x
∀
y
y
x
∈
A
-1
→
y
x
∈
B
∘
C
-1
19
1
4
18
3bitr4i
⊢
A
-1
⊆
B
∘
C
-1
↔
∀
x
∀
y
∃
z
x
A
y
→
x
C
z
∧
z
B
y