| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-fun 6562 | . 2
⊢ (Fun
𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )) | 
| 2 |  | cotrg 6126 | . . . 4
⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧)) | 
| 3 |  | breq1 5145 | . . . . . . . . 9
⊢ (𝑦 = 𝑤 → (𝑦◡𝐴𝑥 ↔ 𝑤◡𝐴𝑥)) | 
| 4 | 3 | anbi1d 631 | . . . . . . . 8
⊢ (𝑦 = 𝑤 → ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧))) | 
| 5 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑦 = 𝑤 → (𝑦 I 𝑧 ↔ 𝑤 I 𝑧)) | 
| 6 | 4, 5 | imbi12d 344 | . . . . . . 7
⊢ (𝑦 = 𝑤 → (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑤 I 𝑧))) | 
| 7 | 6 | albidv 1919 | . . . . . 6
⊢ (𝑦 = 𝑤 → (∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑧((𝑤◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑤 I 𝑧))) | 
| 8 |  | breq2 5146 | . . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑦◡𝐴𝑥 ↔ 𝑦◡𝐴𝑤)) | 
| 9 |  | breq1 5145 | . . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝑥𝐴𝑧 ↔ 𝑤𝐴𝑧)) | 
| 10 | 8, 9 | anbi12d 632 | . . . . . . . 8
⊢ (𝑥 = 𝑤 → ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧))) | 
| 11 | 10 | imbi1d 341 | . . . . . . 7
⊢ (𝑥 = 𝑤 → (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧) → 𝑦 I 𝑧))) | 
| 12 | 11 | albidv 1919 | . . . . . 6
⊢ (𝑥 = 𝑤 → (∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑧((𝑦◡𝐴𝑤 ∧ 𝑤𝐴𝑧) → 𝑦 I 𝑧))) | 
| 13 | 7, 12 | alcomw 2043 | . . . . 5
⊢
(∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧)) | 
| 14 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑦 ∈ V | 
| 15 |  | vex 3483 | . . . . . . . . 9
⊢ 𝑥 ∈ V | 
| 16 | 14, 15 | brcnv 5892 | . . . . . . . 8
⊢ (𝑦◡𝐴𝑥 ↔ 𝑥𝐴𝑦) | 
| 17 | 16 | anbi1i 624 | . . . . . . 7
⊢ ((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) ↔ (𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧)) | 
| 18 |  | vex 3483 | . . . . . . . 8
⊢ 𝑧 ∈ V | 
| 19 | 18 | ideq 5862 | . . . . . . 7
⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧) | 
| 20 | 17, 19 | imbi12i 350 | . . . . . 6
⊢ (((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) | 
| 21 | 20 | 3albii 1820 | . . . . 5
⊢
(∀𝑥∀𝑦∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) | 
| 22 | 13, 21 | bitri 275 | . . . 4
⊢
(∀𝑦∀𝑥∀𝑧((𝑦◡𝐴𝑥 ∧ 𝑥𝐴𝑧) → 𝑦 I 𝑧) ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) | 
| 23 | 2, 22 | bitri 275 | . . 3
⊢ ((𝐴 ∘ ◡𝐴) ⊆ I ↔ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧)) | 
| 24 | 23 | anbi2i 623 | . 2
⊢ ((Rel
𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ) ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) | 
| 25 | 1, 24 | bitri 275 | 1
⊢ (Fun
𝐴 ↔ (Rel 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝐴𝑦 ∧ 𝑥𝐴𝑧) → 𝑦 = 𝑧))) |