Step |
Hyp |
Ref |
Expression |
1 |
|
brcoffn.c |
⊢ ( 𝜑 → 𝐶 Fn 𝑌 ) |
2 |
|
brcoffn.d |
⊢ ( 𝜑 → 𝐷 : 𝑋 ⟶ 𝑌 ) |
3 |
|
brcoffn.r |
⊢ ( 𝜑 → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ) |
4 |
|
fnfco |
⊢ ( ( 𝐶 Fn 𝑌 ∧ 𝐷 : 𝑋 ⟶ 𝑌 ) → ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) |
5 |
1 2 4
|
syl2anc |
⊢ ( 𝜑 → ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) |
6 |
|
simpl |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) → 𝜑 ) |
7 |
|
simpr |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) → ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) |
8 |
6 3
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ) |
9 |
|
fnbr |
⊢ ( ( ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ) → 𝐴 ∈ 𝑋 ) |
10 |
7 8 9
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) → 𝐴 ∈ 𝑋 ) |
11 |
6 7 10
|
3jca |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ) → ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) |
12 |
5 11
|
mpdan |
⊢ ( 𝜑 → ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) |
13 |
2
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐷 : 𝑋 ⟶ 𝑌 ) |
14 |
|
simp3 |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 ) |
15 |
|
fvco3 |
⊢ ( ( 𝐷 : 𝑋 ⟶ 𝑌 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐶 ∘ 𝐷 ) ‘ 𝐴 ) = ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) ) |
16 |
13 14 15
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐶 ∘ 𝐷 ) ‘ 𝐴 ) = ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) ) |
17 |
3
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ) |
18 |
|
fnbrfvb |
⊢ ( ( ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝐶 ∘ 𝐷 ) ‘ 𝐴 ) = 𝐵 ↔ 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ) ) |
19 |
18
|
3adant1 |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝐶 ∘ 𝐷 ) ‘ 𝐴 ) = 𝐵 ↔ 𝐴 ( 𝐶 ∘ 𝐷 ) 𝐵 ) ) |
20 |
17 19
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐶 ∘ 𝐷 ) ‘ 𝐴 ) = 𝐵 ) |
21 |
16 20
|
eqtr3d |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ) |
22 |
|
eqid |
⊢ ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐴 ) |
23 |
21 22
|
jctil |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ) ) |
24 |
13
|
ffnd |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐷 Fn 𝑋 ) |
25 |
|
fnbrfvb |
⊢ ( ( 𝐷 Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐴 ) ↔ 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ) ) |
26 |
24 14 25
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐴 ) ↔ 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ) ) |
27 |
1
|
3ad2ant1 |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐶 Fn 𝑌 ) |
28 |
13 14
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐷 ‘ 𝐴 ) ∈ 𝑌 ) |
29 |
|
fnbrfvb |
⊢ ( ( 𝐶 Fn 𝑌 ∧ ( 𝐷 ‘ 𝐴 ) ∈ 𝑌 ) → ( ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ↔ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) ) |
30 |
27 28 29
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ↔ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) ) |
31 |
26 30
|
anbi12d |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐶 ‘ ( 𝐷 ‘ 𝐴 ) ) = 𝐵 ) ↔ ( 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) ) ) |
32 |
23 31
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝐶 ∘ 𝐷 ) Fn 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) ) |
33 |
12 32
|
syl |
⊢ ( 𝜑 → ( 𝐴 𝐷 ( 𝐷 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐴 ) 𝐶 𝐵 ) ) |