Proof of Theorem asymref
Step | Hyp | Ref
| Expression |
1 | | df-br 3756 |
. . . . . . . . . . 11
⊢ (x𝑅y ↔
〈x, y〉 ∈ 𝑅) |
2 | | vex 2554 |
. . . . . . . . . . . 12
⊢ x ∈
V |
3 | | vex 2554 |
. . . . . . . . . . . 12
⊢ y ∈
V |
4 | 2, 3 | opeluu 4148 |
. . . . . . . . . . 11
⊢
(〈x, y〉 ∈ 𝑅 → (x ∈ ∪ ∪ 𝑅 ∧ y ∈ ∪ ∪ 𝑅)) |
5 | 1, 4 | sylbi 114 |
. . . . . . . . . 10
⊢ (x𝑅y →
(x ∈
∪ ∪ 𝑅 ∧ y ∈ ∪ ∪ 𝑅)) |
6 | 5 | simpld 105 |
. . . . . . . . 9
⊢ (x𝑅y →
x ∈ ∪ ∪ 𝑅) |
7 | 6 | adantr 261 |
. . . . . . . 8
⊢
((x𝑅y ∧ y𝑅x) → x
∈ ∪ ∪ 𝑅) |
8 | 7 | pm4.71ri 372 |
. . . . . . 7
⊢
((x𝑅y ∧ y𝑅x) ↔ (x
∈ ∪ ∪ 𝑅
∧ (x𝑅y ∧ y𝑅x))) |
9 | 8 | bibi1i 217 |
. . . . . 6
⊢
(((x𝑅y ∧ y𝑅x) ↔ (x
∈ ∪ ∪ 𝑅
∧ x =
y)) ↔ ((x ∈ ∪ ∪ 𝑅 ∧
(x𝑅y ∧ y𝑅x)) ↔ (x
∈ ∪ ∪ 𝑅
∧ x =
y))) |
10 | | elin 3120 |
. . . . . . . 8
⊢
(〈x, y〉 ∈ (𝑅 ∩ ◡𝑅) ↔ (〈x, y〉 ∈ 𝑅 ∧
〈x, y〉 ∈ ◡𝑅)) |
11 | 2, 3 | brcnv 4461 |
. . . . . . . . . 10
⊢ (x◡𝑅y ↔ y𝑅x) |
12 | | df-br 3756 |
. . . . . . . . . 10
⊢ (x◡𝑅y ↔ 〈x, y〉 ∈ ◡𝑅) |
13 | 11, 12 | bitr3i 175 |
. . . . . . . . 9
⊢ (y𝑅x ↔
〈x, y〉 ∈ ◡𝑅) |
14 | 1, 13 | anbi12i 433 |
. . . . . . . 8
⊢
((x𝑅y ∧ y𝑅x) ↔ (〈x, y〉 ∈ 𝑅 ∧
〈x, y〉 ∈ ◡𝑅)) |
15 | 10, 14 | bitr4i 176 |
. . . . . . 7
⊢
(〈x, y〉 ∈ (𝑅 ∩ ◡𝑅) ↔ (x𝑅y ∧ y𝑅x)) |
16 | 3 | opelres 4560 |
. . . . . . . 8
⊢
(〈x, y〉 ∈ ( I
↾ ∪ ∪ 𝑅) ↔ (〈x, y〉 ∈ I ∧ x ∈ ∪ ∪ 𝑅)) |
17 | | df-br 3756 |
. . . . . . . . . 10
⊢ (x I y ↔
〈x, y〉 ∈ I
) |
18 | 3 | ideq 4431 |
. . . . . . . . . 10
⊢ (x I y ↔
x = y) |
19 | 17, 18 | bitr3i 175 |
. . . . . . . . 9
⊢
(〈x, y〉 ∈ I ↔
x = y) |
20 | 19 | anbi2ci 432 |
. . . . . . . 8
⊢
((〈x, y〉 ∈ I ∧ x ∈ ∪ ∪ 𝑅)
↔ (x ∈ ∪ ∪ 𝑅
∧ x =
y)) |
21 | 16, 20 | bitri 173 |
. . . . . . 7
⊢
(〈x, y〉 ∈ ( I
↾ ∪ ∪ 𝑅) ↔ (x ∈ ∪ ∪ 𝑅 ∧ x = y)) |
22 | 15, 21 | bibi12i 218 |
. . . . . 6
⊢
((〈x, y〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈x, y〉 ∈ ( I ↾ ∪ ∪ 𝑅))
↔ ((x𝑅y ∧ y𝑅x) ↔ (x
∈ ∪ ∪ 𝑅
∧ x =
y))) |
23 | | pm5.32 426 |
. . . . . 6
⊢
((x ∈ ∪ ∪ 𝑅
→ ((x𝑅y ∧ y𝑅x) ↔ x =
y)) ↔ ((x ∈ ∪ ∪ 𝑅 ∧
(x𝑅y ∧ y𝑅x)) ↔ (x
∈ ∪ ∪ 𝑅
∧ x =
y))) |
24 | 9, 22, 23 | 3bitr4i 201 |
. . . . 5
⊢
((〈x, y〉 ∈ (𝑅 ∩ ◡𝑅) ↔ 〈x, y〉 ∈ ( I ↾ ∪ ∪ 𝑅))
↔ (x ∈ ∪ ∪ 𝑅
→ ((x𝑅y ∧ y𝑅x) ↔ x =
y))) |
25 | 24 | albii 1356 |
. . . 4
⊢ (∀y(〈x,
y〉 ∈
(𝑅 ∩ ◡𝑅) ↔ 〈x, y〉 ∈ ( I ↾ ∪ ∪ 𝑅))
↔ ∀y(x ∈ ∪ ∪ 𝑅
→ ((x𝑅y ∧ y𝑅x) ↔ x =
y))) |
26 | | 19.21v 1750 |
. . . 4
⊢ (∀y(x ∈ ∪ ∪ 𝑅 → ((x𝑅y ∧ y𝑅x) ↔ x =
y)) ↔ (x ∈ ∪ ∪ 𝑅 → ∀y((x𝑅y ∧ y𝑅x) ↔ x =
y))) |
27 | 25, 26 | bitri 173 |
. . 3
⊢ (∀y(〈x,
y〉 ∈
(𝑅 ∩ ◡𝑅) ↔ 〈x, y〉 ∈ ( I ↾ ∪ ∪ 𝑅))
↔ (x ∈ ∪ ∪ 𝑅
→ ∀y((x𝑅y ∧ y𝑅x)
↔ x = y))) |
28 | 27 | albii 1356 |
. 2
⊢ (∀x∀y(〈x,
y〉 ∈
(𝑅 ∩ ◡𝑅) ↔ 〈x, y〉 ∈ ( I ↾ ∪ ∪ 𝑅))
↔ ∀x(x ∈ ∪ ∪ 𝑅
→ ∀y((x𝑅y ∧ y𝑅x)
↔ x = y))) |
29 | | relcnv 4646 |
. . . 4
⊢ Rel ◡𝑅 |
30 | | relin2 4399 |
. . . 4
⊢ (Rel
◡𝑅 → Rel (𝑅 ∩ ◡𝑅)) |
31 | 29, 30 | ax-mp 7 |
. . 3
⊢ Rel
(𝑅 ∩ ◡𝑅) |
32 | | relres 4582 |
. . 3
⊢ Rel ( I
↾ ∪ ∪ 𝑅) |
33 | | eqrel 4372 |
. . 3
⊢ ((Rel
(𝑅 ∩ ◡𝑅) ∧ Rel ( I
↾ ∪ ∪ 𝑅)) → ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ ∀x∀y(〈x,
y〉 ∈
(𝑅 ∩ ◡𝑅) ↔ 〈x, y〉 ∈ ( I ↾ ∪ ∪ 𝑅)))) |
34 | 31, 32, 33 | mp2an 402 |
. 2
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ ∀x∀y(〈x,
y〉 ∈
(𝑅 ∩ ◡𝑅) ↔ 〈x, y〉 ∈ ( I ↾ ∪ ∪ 𝑅))) |
35 | | df-ral 2305 |
. 2
⊢ (∀x ∈ ∪ ∪ 𝑅∀y((x𝑅y ∧ y𝑅x) ↔ x =
y) ↔ ∀x(x ∈ ∪ ∪ 𝑅 → ∀y((x𝑅y ∧ y𝑅x) ↔ x =
y))) |
36 | 28, 34, 35 | 3bitr4i 201 |
1
⊢ ((𝑅 ∩ ◡𝑅) = ( I ↾ ∪
∪ 𝑅) ↔ ∀x ∈ ∪ ∪ 𝑅∀y((x𝑅y ∧ y𝑅x) ↔ x =
y)) |