Metamath Proof Explorer

Theorem brco3f1o

Description: Conditions allowing the decomposition of a binary relation. (Contributed by RP, 8-Jun-2021)

Ref Expression
Hypotheses brco3f1o.c ⊢ ( 𝜑 → 𝐶 : 𝑌 –1-1-onto→ 𝑍 )
brco3f1o.d ⊢ ( 𝜑 → 𝐷 : 𝑋 –1-1-onto→ 𝑌 )
brco3f1o.e ⊢ ( 𝜑 → 𝐸 : 𝑊 –1-1-onto→ 𝑋 )
brco3f1o.r ⊢ ( 𝜑 → 𝐴 ( 𝐶 ∘ ( 𝐷 ∘ 𝐸 ) ) 𝐵 )
Assertion brco3f1o ( 𝜑 → ( ( ◡ 𝐶 ‘ 𝐵 ) 𝐶 𝐵 ∧ ( ◡ 𝐷 ‘ ( ◡ 𝐶 ‘ 𝐵 ) ) 𝐷 ( ◡ 𝐶 ‘ 𝐵 ) ∧ 𝐴 𝐸 ( ◡ 𝐷 ‘ ( ◡ 𝐶 ‘ 𝐵 ) ) ) )

Proof

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