Step | Hyp | Ref
| Expression |
1 | | alcom 2157 |
. 2
⊢
(∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑏∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐))) |
2 | | 19.21v 1943 |
. . . . . . 7
⊢
(∀𝑎(𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ (𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐))) |
3 | | impexp 452 |
. . . . . . . . 9
⊢ (((𝑏𝑅𝑐 ∧ 𝑏𝑅𝑎) → 𝑎 = 𝑐) ↔ (𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐))) |
4 | | vex 3452 |
. . . . . . . . . . . . 13
⊢ 𝑏 ∈ V |
5 | | vex 3452 |
. . . . . . . . . . . . 13
⊢ 𝑐 ∈ V |
6 | 4, 5 | brcnv 5843 |
. . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑐 ↔ 𝑐◡𝑅𝑏) |
7 | | df-br 5111 |
. . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑐 ↔ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) |
8 | 5, 4 | brcnv 5843 |
. . . . . . . . . . . 12
⊢ (𝑐◡𝑅𝑏 ↔ 𝑏𝑅𝑐) |
9 | 6, 7, 8 | 3bitr3ri 302 |
. . . . . . . . . . 11
⊢ (𝑏𝑅𝑐 ↔ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) |
10 | | vex 3452 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
11 | 4, 10 | brcnv 5843 |
. . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑎 ↔ 𝑎◡𝑅𝑏) |
12 | | df-br 5111 |
. . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑎 ↔ ⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅) |
13 | 10, 4 | brcnv 5843 |
. . . . . . . . . . . 12
⊢ (𝑎◡𝑅𝑏 ↔ 𝑏𝑅𝑎) |
14 | 11, 12, 13 | 3bitr3ri 302 |
. . . . . . . . . . 11
⊢ (𝑏𝑅𝑎 ↔ ⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅) |
15 | 9, 14 | anbi12ci 629 |
. . . . . . . . . 10
⊢ ((𝑏𝑅𝑐 ∧ 𝑏𝑅𝑎) ↔ (⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅)) |
16 | 15 | imbi1i 350 |
. . . . . . . . 9
⊢ (((𝑏𝑅𝑐 ∧ 𝑏𝑅𝑎) → 𝑎 = 𝑐) ↔ ((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
17 | 3, 16 | bitr3i 277 |
. . . . . . . 8
⊢ ((𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
18 | 17 | albii 1822 |
. . . . . . 7
⊢
(∀𝑎(𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑎((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
19 | 2, 18 | bitr3i 277 |
. . . . . 6
⊢ ((𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑎((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
20 | 19 | albii 1822 |
. . . . 5
⊢
(∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑐∀𝑎((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
21 | | alcom 2157 |
. . . . 5
⊢
(∀𝑐∀𝑎((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐) ↔ ∀𝑎∀𝑐((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
22 | 20, 21 | bitri 275 |
. . . 4
⊢
(∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑎∀𝑐((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
23 | | opeq2 4836 |
. . . . . 6
⊢ (𝑎 = 𝑐 → ⟨𝑏, 𝑎⟩ = ⟨𝑏, 𝑐⟩) |
24 | 23 | eleq1d 2823 |
. . . . 5
⊢ (𝑎 = 𝑐 → (⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ↔ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅)) |
25 | 24 | mo4 2565 |
. . . 4
⊢
(∃*𝑎⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ↔ ∀𝑎∀𝑐((⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ∧ ⟨𝑏, 𝑐⟩ ∈ ◡◡𝑅) → 𝑎 = 𝑐)) |
26 | | df-mo 2539 |
. . . 4
⊢
(∃*𝑎⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 ↔ ∃𝑐∀𝑎(⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 → 𝑎 = 𝑐)) |
27 | 22, 25, 26 | 3bitr2i 299 |
. . 3
⊢
(∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∃𝑐∀𝑎(⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 → 𝑎 = 𝑐)) |
28 | 27 | albii 1822 |
. 2
⊢
(∀𝑏∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑏∃𝑐∀𝑎(⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 → 𝑎 = 𝑐)) |
29 | | relcnv 6061 |
. . . 4
⊢ Rel ◡◡𝑅 |
30 | 29 | biantrur 532 |
. . 3
⊢
(∀𝑏∃𝑐∀𝑎(⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 → 𝑎 = 𝑐) ↔ (Rel ◡◡𝑅 ∧ ∀𝑏∃𝑐∀𝑎(⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 → 𝑎 = 𝑐))) |
31 | | dffun5 6518 |
. . 3
⊢ (Fun
◡◡𝑅 ↔ (Rel ◡◡𝑅 ∧ ∀𝑏∃𝑐∀𝑎(⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 → 𝑎 = 𝑐))) |
32 | 30, 31 | bitr4i 278 |
. 2
⊢
(∀𝑏∃𝑐∀𝑎(⟨𝑏, 𝑎⟩ ∈ ◡◡𝑅 → 𝑎 = 𝑐) ↔ Fun ◡◡𝑅) |
33 | 1, 28, 32 | 3bitri 297 |
1
⊢
(∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ Fun ◡◡𝑅) |