Proof of Theorem dffrege115
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | alcom 2158 | . 2
⊢
(∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑏∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐))) | 
| 2 |  | 19.21v 1938 | . . . . . . 7
⊢
(∀𝑎(𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ (𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐))) | 
| 3 |  | impexp 450 | . . . . . . . . 9
⊢ (((𝑏𝑅𝑐 ∧ 𝑏𝑅𝑎) → 𝑎 = 𝑐) ↔ (𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐))) | 
| 4 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑏 ∈ V | 
| 5 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑐 ∈ V | 
| 6 | 4, 5 | brcnv 5892 | . . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑐 ↔ 𝑐◡𝑅𝑏) | 
| 7 |  | df-br 5143 | . . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑐 ↔ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) | 
| 8 | 5, 4 | brcnv 5892 | . . . . . . . . . . . 12
⊢ (𝑐◡𝑅𝑏 ↔ 𝑏𝑅𝑐) | 
| 9 | 6, 7, 8 | 3bitr3ri 302 | . . . . . . . . . . 11
⊢ (𝑏𝑅𝑐 ↔ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) | 
| 10 |  | vex 3483 | . . . . . . . . . . . . 13
⊢ 𝑎 ∈ V | 
| 11 | 4, 10 | brcnv 5892 | . . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑎 ↔ 𝑎◡𝑅𝑏) | 
| 12 |  | df-br 5143 | . . . . . . . . . . . 12
⊢ (𝑏◡◡𝑅𝑎 ↔ 〈𝑏, 𝑎〉 ∈ ◡◡𝑅) | 
| 13 | 10, 4 | brcnv 5892 | . . . . . . . . . . . 12
⊢ (𝑎◡𝑅𝑏 ↔ 𝑏𝑅𝑎) | 
| 14 | 11, 12, 13 | 3bitr3ri 302 | . . . . . . . . . . 11
⊢ (𝑏𝑅𝑎 ↔ 〈𝑏, 𝑎〉 ∈ ◡◡𝑅) | 
| 15 | 9, 14 | anbi12ci 629 | . . . . . . . . . 10
⊢ ((𝑏𝑅𝑐 ∧ 𝑏𝑅𝑎) ↔ (〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅)) | 
| 16 | 15 | imbi1i 349 | . . . . . . . . 9
⊢ (((𝑏𝑅𝑐 ∧ 𝑏𝑅𝑎) → 𝑎 = 𝑐) ↔ ((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 17 | 3, 16 | bitr3i 277 | . . . . . . . 8
⊢ ((𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 18 | 17 | albii 1818 | . . . . . . 7
⊢
(∀𝑎(𝑏𝑅𝑐 → (𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑎((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 19 | 2, 18 | bitr3i 277 | . . . . . 6
⊢ ((𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑎((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 20 | 19 | albii 1818 | . . . . 5
⊢
(∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑐∀𝑎((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 21 |  | alcom 2158 | . . . . 5
⊢
(∀𝑐∀𝑎((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐) ↔ ∀𝑎∀𝑐((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 22 | 20, 21 | bitri 275 | . . . 4
⊢
(∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑎∀𝑐((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 23 |  | opeq2 4873 | . . . . . 6
⊢ (𝑎 = 𝑐 → 〈𝑏, 𝑎〉 = 〈𝑏, 𝑐〉) | 
| 24 | 23 | eleq1d 2825 | . . . . 5
⊢ (𝑎 = 𝑐 → (〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ↔ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅)) | 
| 25 | 24 | mo4 2565 | . . . 4
⊢
(∃*𝑎〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ↔ ∀𝑎∀𝑐((〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ∧ 〈𝑏, 𝑐〉 ∈ ◡◡𝑅) → 𝑎 = 𝑐)) | 
| 26 |  | df-mo 2539 | . . . 4
⊢
(∃*𝑎〈𝑏, 𝑎〉 ∈ ◡◡𝑅 ↔ ∃𝑐∀𝑎(〈𝑏, 𝑎〉 ∈ ◡◡𝑅 → 𝑎 = 𝑐)) | 
| 27 | 22, 25, 26 | 3bitr2i 299 | . . 3
⊢
(∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∃𝑐∀𝑎(〈𝑏, 𝑎〉 ∈ ◡◡𝑅 → 𝑎 = 𝑐)) | 
| 28 | 27 | albii 1818 | . 2
⊢
(∀𝑏∀𝑐(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ ∀𝑏∃𝑐∀𝑎(〈𝑏, 𝑎〉 ∈ ◡◡𝑅 → 𝑎 = 𝑐)) | 
| 29 |  | relcnv 6121 | . . . 4
⊢ Rel ◡◡𝑅 | 
| 30 | 29 | biantrur 530 | . . 3
⊢
(∀𝑏∃𝑐∀𝑎(〈𝑏, 𝑎〉 ∈ ◡◡𝑅 → 𝑎 = 𝑐) ↔ (Rel ◡◡𝑅 ∧ ∀𝑏∃𝑐∀𝑎(〈𝑏, 𝑎〉 ∈ ◡◡𝑅 → 𝑎 = 𝑐))) | 
| 31 |  | dffun5 6577 | . . 3
⊢ (Fun
◡◡𝑅 ↔ (Rel ◡◡𝑅 ∧ ∀𝑏∃𝑐∀𝑎(〈𝑏, 𝑎〉 ∈ ◡◡𝑅 → 𝑎 = 𝑐))) | 
| 32 | 30, 31 | bitr4i 278 | . 2
⊢
(∀𝑏∃𝑐∀𝑎(〈𝑏, 𝑎〉 ∈ ◡◡𝑅 → 𝑎 = 𝑐) ↔ Fun ◡◡𝑅) | 
| 33 | 1, 28, 32 | 3bitri 297 | 1
⊢
(∀𝑐∀𝑏(𝑏𝑅𝑐 → ∀𝑎(𝑏𝑅𝑎 → 𝑎 = 𝑐)) ↔ Fun ◡◡𝑅) |