Step |
Hyp |
Ref |
Expression |
1 |
|
cossssid3 |
⊢ ( ≀ ◡ 𝑅 ⊆ I ↔ ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑥 ◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ) |
2 |
|
alrot3 |
⊢ ( ∀ 𝑥 ∀ 𝑢 ∀ 𝑣 ( ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑥 ◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑥 ◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ) |
3 |
|
brcnvg |
⊢ ( ( 𝑥 ∈ V ∧ 𝑢 ∈ V ) → ( 𝑥 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 ) ) |
4 |
3
|
el2v |
⊢ ( 𝑥 ◡ 𝑅 𝑢 ↔ 𝑢 𝑅 𝑥 ) |
5 |
|
brcnvg |
⊢ ( ( 𝑥 ∈ V ∧ 𝑣 ∈ V ) → ( 𝑥 ◡ 𝑅 𝑣 ↔ 𝑣 𝑅 𝑥 ) ) |
6 |
5
|
el2v |
⊢ ( 𝑥 ◡ 𝑅 𝑣 ↔ 𝑣 𝑅 𝑥 ) |
7 |
4 6
|
anbi12i |
⊢ ( ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑥 ◡ 𝑅 𝑣 ) ↔ ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) ) |
8 |
7
|
imbi1i |
⊢ ( ( ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑥 ◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ↔ ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) ) |
9 |
8
|
3albii |
⊢ ( ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑥 ◡ 𝑅 𝑢 ∧ 𝑥 ◡ 𝑅 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) ) |
10 |
1 2 9
|
3bitri |
⊢ ( ≀ ◡ 𝑅 ⊆ I ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑅 𝑥 ∧ 𝑣 𝑅 𝑥 ) → 𝑢 = 𝑣 ) ) |