Proof of Theorem brco3f1o
| Step | Hyp | Ref
| Expression |
| 1 | | brco3f1o.e |
. . . 4
⊢ (𝜑 → 𝐸:𝑊–1-1-onto→𝑋) |
| 2 | | f1ocnv 6860 |
. . . 4
⊢ (𝐸:𝑊–1-1-onto→𝑋 → ◡𝐸:𝑋–1-1-onto→𝑊) |
| 3 | | f1ofn 6849 |
. . . 4
⊢ (◡𝐸:𝑋–1-1-onto→𝑊 → ◡𝐸 Fn 𝑋) |
| 4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝜑 → ◡𝐸 Fn 𝑋) |
| 5 | | brco3f1o.d |
. . . 4
⊢ (𝜑 → 𝐷:𝑋–1-1-onto→𝑌) |
| 6 | | f1ocnv 6860 |
. . . 4
⊢ (𝐷:𝑋–1-1-onto→𝑌 → ◡𝐷:𝑌–1-1-onto→𝑋) |
| 7 | | f1of 6848 |
. . . 4
⊢ (◡𝐷:𝑌–1-1-onto→𝑋 → ◡𝐷:𝑌⟶𝑋) |
| 8 | 5, 6, 7 | 3syl 18 |
. . 3
⊢ (𝜑 → ◡𝐷:𝑌⟶𝑋) |
| 9 | | brco3f1o.c |
. . . 4
⊢ (𝜑 → 𝐶:𝑌–1-1-onto→𝑍) |
| 10 | | f1ocnv 6860 |
. . . 4
⊢ (𝐶:𝑌–1-1-onto→𝑍 → ◡𝐶:𝑍–1-1-onto→𝑌) |
| 11 | | f1of 6848 |
. . . 4
⊢ (◡𝐶:𝑍–1-1-onto→𝑌 → ◡𝐶:𝑍⟶𝑌) |
| 12 | 9, 10, 11 | 3syl 18 |
. . 3
⊢ (𝜑 → ◡𝐶:𝑍⟶𝑌) |
| 13 | | brco3f1o.r |
. . . 4
⊢ (𝜑 → 𝐴(𝐶 ∘ (𝐷 ∘ 𝐸))𝐵) |
| 14 | | relco 6126 |
. . . . . 6
⊢ Rel
((𝐶 ∘ 𝐷) ∘ 𝐸) |
| 15 | 14 | relbrcnv 6125 |
. . . . 5
⊢ (𝐵◡((𝐶 ∘ 𝐷) ∘ 𝐸)𝐴 ↔ 𝐴((𝐶 ∘ 𝐷) ∘ 𝐸)𝐵) |
| 16 | | cnvco 5896 |
. . . . . . 7
⊢ ◡((𝐶 ∘ 𝐷) ∘ 𝐸) = (◡𝐸 ∘ ◡(𝐶 ∘ 𝐷)) |
| 17 | | cnvco 5896 |
. . . . . . . 8
⊢ ◡(𝐶 ∘ 𝐷) = (◡𝐷 ∘ ◡𝐶) |
| 18 | 17 | coeq2i 5871 |
. . . . . . 7
⊢ (◡𝐸 ∘ ◡(𝐶 ∘ 𝐷)) = (◡𝐸 ∘ (◡𝐷 ∘ ◡𝐶)) |
| 19 | 16, 18 | eqtri 2765 |
. . . . . 6
⊢ ◡((𝐶 ∘ 𝐷) ∘ 𝐸) = (◡𝐸 ∘ (◡𝐷 ∘ ◡𝐶)) |
| 20 | 19 | breqi 5149 |
. . . . 5
⊢ (𝐵◡((𝐶 ∘ 𝐷) ∘ 𝐸)𝐴 ↔ 𝐵(◡𝐸 ∘ (◡𝐷 ∘ ◡𝐶))𝐴) |
| 21 | | coass 6285 |
. . . . . 6
⊢ ((𝐶 ∘ 𝐷) ∘ 𝐸) = (𝐶 ∘ (𝐷 ∘ 𝐸)) |
| 22 | 21 | breqi 5149 |
. . . . 5
⊢ (𝐴((𝐶 ∘ 𝐷) ∘ 𝐸)𝐵 ↔ 𝐴(𝐶 ∘ (𝐷 ∘ 𝐸))𝐵) |
| 23 | 15, 20, 22 | 3bitr3ri 302 |
. . . 4
⊢ (𝐴(𝐶 ∘ (𝐷 ∘ 𝐸))𝐵 ↔ 𝐵(◡𝐸 ∘ (◡𝐷 ∘ ◡𝐶))𝐴) |
| 24 | 13, 23 | sylib 218 |
. . 3
⊢ (𝜑 → 𝐵(◡𝐸 ∘ (◡𝐷 ∘ ◡𝐶))𝐴) |
| 25 | 4, 8, 12, 24 | brcofffn 44044 |
. 2
⊢ (𝜑 → (𝐵◡𝐶(◡𝐶‘𝐵) ∧ (◡𝐶‘𝐵)◡𝐷(◡𝐷‘(◡𝐶‘𝐵)) ∧ (◡𝐷‘(◡𝐶‘𝐵))◡𝐸𝐴)) |
| 26 | | f1orel 6851 |
. . . 4
⊢ (𝐶:𝑌–1-1-onto→𝑍 → Rel 𝐶) |
| 27 | | relbrcnvg 6123 |
. . . 4
⊢ (Rel
𝐶 → (𝐵◡𝐶(◡𝐶‘𝐵) ↔ (◡𝐶‘𝐵)𝐶𝐵)) |
| 28 | 9, 26, 27 | 3syl 18 |
. . 3
⊢ (𝜑 → (𝐵◡𝐶(◡𝐶‘𝐵) ↔ (◡𝐶‘𝐵)𝐶𝐵)) |
| 29 | | f1orel 6851 |
. . . 4
⊢ (𝐷:𝑋–1-1-onto→𝑌 → Rel 𝐷) |
| 30 | | relbrcnvg 6123 |
. . . 4
⊢ (Rel
𝐷 → ((◡𝐶‘𝐵)◡𝐷(◡𝐷‘(◡𝐶‘𝐵)) ↔ (◡𝐷‘(◡𝐶‘𝐵))𝐷(◡𝐶‘𝐵))) |
| 31 | 5, 29, 30 | 3syl 18 |
. . 3
⊢ (𝜑 → ((◡𝐶‘𝐵)◡𝐷(◡𝐷‘(◡𝐶‘𝐵)) ↔ (◡𝐷‘(◡𝐶‘𝐵))𝐷(◡𝐶‘𝐵))) |
| 32 | | f1orel 6851 |
. . . 4
⊢ (𝐸:𝑊–1-1-onto→𝑋 → Rel 𝐸) |
| 33 | | relbrcnvg 6123 |
. . . 4
⊢ (Rel
𝐸 → ((◡𝐷‘(◡𝐶‘𝐵))◡𝐸𝐴 ↔ 𝐴𝐸(◡𝐷‘(◡𝐶‘𝐵)))) |
| 34 | 1, 32, 33 | 3syl 18 |
. . 3
⊢ (𝜑 → ((◡𝐷‘(◡𝐶‘𝐵))◡𝐸𝐴 ↔ 𝐴𝐸(◡𝐷‘(◡𝐶‘𝐵)))) |
| 35 | 28, 31, 34 | 3anbi123d 1438 |
. 2
⊢ (𝜑 → ((𝐵◡𝐶(◡𝐶‘𝐵) ∧ (◡𝐶‘𝐵)◡𝐷(◡𝐷‘(◡𝐶‘𝐵)) ∧ (◡𝐷‘(◡𝐶‘𝐵))◡𝐸𝐴) ↔ ((◡𝐶‘𝐵)𝐶𝐵 ∧ (◡𝐷‘(◡𝐶‘𝐵))𝐷(◡𝐶‘𝐵) ∧ 𝐴𝐸(◡𝐷‘(◡𝐶‘𝐵))))) |
| 36 | 25, 35 | mpbid 232 |
1
⊢ (𝜑 → ((◡𝐶‘𝐵)𝐶𝐵 ∧ (◡𝐷‘(◡𝐶‘𝐵))𝐷(◡𝐶‘𝐵) ∧ 𝐴𝐸(◡𝐷‘(◡𝐶‘𝐵)))) |