Step |
Hyp |
Ref |
Expression |
1 |
|
fcobij.1 |
⊢ ( 𝜑 → 𝐺 : 𝑆 –1-1-onto→ 𝑇 ) |
2 |
|
fcobij.2 |
⊢ ( 𝜑 → 𝑅 ∈ 𝑈 ) |
3 |
|
fcobij.3 |
⊢ ( 𝜑 → 𝑆 ∈ 𝑉 ) |
4 |
|
fcobij.4 |
⊢ ( 𝜑 → 𝑇 ∈ 𝑊 ) |
5 |
|
eqid |
⊢ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ↦ ( 𝐺 ∘ 𝑓 ) ) = ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ↦ ( 𝐺 ∘ 𝑓 ) ) |
6 |
|
f1of |
⊢ ( 𝐺 : 𝑆 –1-1-onto→ 𝑇 → 𝐺 : 𝑆 ⟶ 𝑇 ) |
7 |
1 6
|
syl |
⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ 𝑇 ) |
8 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → 𝐺 : 𝑆 ⟶ 𝑇 ) |
9 |
3 2
|
elmapd |
⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ↔ 𝑓 : 𝑅 ⟶ 𝑆 ) ) |
10 |
9
|
biimpa |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → 𝑓 : 𝑅 ⟶ 𝑆 ) |
11 |
|
fco |
⊢ ( ( 𝐺 : 𝑆 ⟶ 𝑇 ∧ 𝑓 : 𝑅 ⟶ 𝑆 ) → ( 𝐺 ∘ 𝑓 ) : 𝑅 ⟶ 𝑇 ) |
12 |
8 10 11
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → ( 𝐺 ∘ 𝑓 ) : 𝑅 ⟶ 𝑇 ) |
13 |
4 2
|
elmapd |
⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝑓 ) ∈ ( 𝑇 ↑m 𝑅 ) ↔ ( 𝐺 ∘ 𝑓 ) : 𝑅 ⟶ 𝑇 ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → ( ( 𝐺 ∘ 𝑓 ) ∈ ( 𝑇 ↑m 𝑅 ) ↔ ( 𝐺 ∘ 𝑓 ) : 𝑅 ⟶ 𝑇 ) ) |
15 |
12 14
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) → ( 𝐺 ∘ 𝑓 ) ∈ ( 𝑇 ↑m 𝑅 ) ) |
16 |
|
f1ocnv |
⊢ ( 𝐺 : 𝑆 –1-1-onto→ 𝑇 → ◡ 𝐺 : 𝑇 –1-1-onto→ 𝑆 ) |
17 |
|
f1of |
⊢ ( ◡ 𝐺 : 𝑇 –1-1-onto→ 𝑆 → ◡ 𝐺 : 𝑇 ⟶ 𝑆 ) |
18 |
1 16 17
|
3syl |
⊢ ( 𝜑 → ◡ 𝐺 : 𝑇 ⟶ 𝑆 ) |
19 |
18
|
adantr |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) → ◡ 𝐺 : 𝑇 ⟶ 𝑆 ) |
20 |
4 2
|
elmapd |
⊢ ( 𝜑 → ( ℎ ∈ ( 𝑇 ↑m 𝑅 ) ↔ ℎ : 𝑅 ⟶ 𝑇 ) ) |
21 |
20
|
biimpa |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) → ℎ : 𝑅 ⟶ 𝑇 ) |
22 |
|
fco |
⊢ ( ( ◡ 𝐺 : 𝑇 ⟶ 𝑆 ∧ ℎ : 𝑅 ⟶ 𝑇 ) → ( ◡ 𝐺 ∘ ℎ ) : 𝑅 ⟶ 𝑆 ) |
23 |
19 21 22
|
syl2anc |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) → ( ◡ 𝐺 ∘ ℎ ) : 𝑅 ⟶ 𝑆 ) |
24 |
3 2
|
elmapd |
⊢ ( 𝜑 → ( ( ◡ 𝐺 ∘ ℎ ) ∈ ( 𝑆 ↑m 𝑅 ) ↔ ( ◡ 𝐺 ∘ ℎ ) : 𝑅 ⟶ 𝑆 ) ) |
25 |
24
|
adantr |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) → ( ( ◡ 𝐺 ∘ ℎ ) ∈ ( 𝑆 ↑m 𝑅 ) ↔ ( ◡ 𝐺 ∘ ℎ ) : 𝑅 ⟶ 𝑆 ) ) |
26 |
23 25
|
mpbird |
⊢ ( ( 𝜑 ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) → ( ◡ 𝐺 ∘ ℎ ) ∈ ( 𝑆 ↑m 𝑅 ) ) |
27 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) |
28 |
27
|
coeq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ( 𝐺 ∘ 𝑓 ) = ( 𝐺 ∘ ( ◡ 𝐺 ∘ ℎ ) ) ) |
29 |
|
coass |
⊢ ( ( 𝐺 ∘ ◡ 𝐺 ) ∘ ℎ ) = ( 𝐺 ∘ ( ◡ 𝐺 ∘ ℎ ) ) |
30 |
28 29
|
eqtr4di |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ( 𝐺 ∘ 𝑓 ) = ( ( 𝐺 ∘ ◡ 𝐺 ) ∘ ℎ ) ) |
31 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → 𝜑 ) |
32 |
|
f1ococnv2 |
⊢ ( 𝐺 : 𝑆 –1-1-onto→ 𝑇 → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ 𝑇 ) ) |
33 |
31 1 32
|
3syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ( 𝐺 ∘ ◡ 𝐺 ) = ( I ↾ 𝑇 ) ) |
34 |
33
|
coeq1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ( ( 𝐺 ∘ ◡ 𝐺 ) ∘ ℎ ) = ( ( I ↾ 𝑇 ) ∘ ℎ ) ) |
35 |
|
simplrr |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) |
36 |
31 35 21
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ℎ : 𝑅 ⟶ 𝑇 ) |
37 |
|
fcoi2 |
⊢ ( ℎ : 𝑅 ⟶ 𝑇 → ( ( I ↾ 𝑇 ) ∘ ℎ ) = ℎ ) |
38 |
36 37
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ( ( I ↾ 𝑇 ) ∘ ℎ ) = ℎ ) |
39 |
30 34 38
|
3eqtrrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) → ℎ = ( 𝐺 ∘ 𝑓 ) ) |
40 |
|
simpr |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → ℎ = ( 𝐺 ∘ 𝑓 ) ) |
41 |
40
|
coeq2d |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → ( ◡ 𝐺 ∘ ℎ ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ 𝑓 ) ) ) |
42 |
|
coass |
⊢ ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ 𝑓 ) = ( ◡ 𝐺 ∘ ( 𝐺 ∘ 𝑓 ) ) |
43 |
41 42
|
eqtr4di |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → ( ◡ 𝐺 ∘ ℎ ) = ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ 𝑓 ) ) |
44 |
|
simpll |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → 𝜑 ) |
45 |
|
f1ococnv1 |
⊢ ( 𝐺 : 𝑆 –1-1-onto→ 𝑇 → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝑆 ) ) |
46 |
44 1 45
|
3syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → ( ◡ 𝐺 ∘ 𝐺 ) = ( I ↾ 𝑆 ) ) |
47 |
46
|
coeq1d |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → ( ( ◡ 𝐺 ∘ 𝐺 ) ∘ 𝑓 ) = ( ( I ↾ 𝑆 ) ∘ 𝑓 ) ) |
48 |
|
simplrl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ) |
49 |
44 48 10
|
syl2anc |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → 𝑓 : 𝑅 ⟶ 𝑆 ) |
50 |
|
fcoi2 |
⊢ ( 𝑓 : 𝑅 ⟶ 𝑆 → ( ( I ↾ 𝑆 ) ∘ 𝑓 ) = 𝑓 ) |
51 |
49 50
|
syl |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → ( ( I ↾ 𝑆 ) ∘ 𝑓 ) = 𝑓 ) |
52 |
43 47 51
|
3eqtrrd |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) ∧ ℎ = ( 𝐺 ∘ 𝑓 ) ) → 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ) |
53 |
39 52
|
impbida |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ∧ ℎ ∈ ( 𝑇 ↑m 𝑅 ) ) ) → ( 𝑓 = ( ◡ 𝐺 ∘ ℎ ) ↔ ℎ = ( 𝐺 ∘ 𝑓 ) ) ) |
54 |
5 15 26 53
|
f1o2d |
⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑆 ↑m 𝑅 ) ↦ ( 𝐺 ∘ 𝑓 ) ) : ( 𝑆 ↑m 𝑅 ) –1-1-onto→ ( 𝑇 ↑m 𝑅 ) ) |