Step |
Hyp |
Ref |
Expression |
1 |
|
cfsetsnfsetfv.f |
⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∃ 𝑏 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( 𝑓 ‘ 𝑧 ) = 𝑏 ) } |
2 |
|
cfsetsnfsetfv.g |
⊢ 𝐺 = { 𝑥 ∣ 𝑥 : { 𝑌 } ⟶ 𝐵 } |
3 |
|
cfsetsnfsetfv.h |
⊢ 𝐻 = ( 𝑔 ∈ 𝐺 ↦ ( 𝑎 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑌 ) ) ) |
4 |
1 2 3
|
cfsetsnfsetf |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 ⟶ 𝐹 ) |
5 |
1 2 3
|
cfsetsnfsetfv |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑚 ∈ 𝐺 ) → ( 𝐻 ‘ 𝑚 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑚 ‘ 𝑌 ) ) ) |
6 |
5
|
ad2ant2r |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( 𝐻 ‘ 𝑚 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑚 ‘ 𝑌 ) ) ) |
7 |
1 2 3
|
cfsetsnfsetfv |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑛 ∈ 𝐺 ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ) |
8 |
7
|
ad2ant2rl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( 𝐻 ‘ 𝑛 ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ) |
9 |
6 8
|
eqeq12d |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( ( 𝐻 ‘ 𝑚 ) = ( 𝐻 ‘ 𝑛 ) ↔ ( 𝑎 ∈ 𝐴 ↦ ( 𝑚 ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ) ) |
10 |
|
fvexd |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑚 ‘ 𝑌 ) ∈ V ) |
11 |
10
|
ralrimiva |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ∀ 𝑎 ∈ 𝐴 ( 𝑚 ‘ 𝑌 ) ∈ V ) |
12 |
|
mpteqb |
⊢ ( ∀ 𝑎 ∈ 𝐴 ( 𝑚 ‘ 𝑌 ) ∈ V → ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑚 ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ↔ ∀ 𝑎 ∈ 𝐴 ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) ) |
13 |
11 12
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑚 ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) ↔ ∀ 𝑎 ∈ 𝐴 ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) ) |
14 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → 𝑌 ∈ 𝐴 ) |
15 |
|
idd |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) ∧ 𝑎 = 𝑌 ) → ( ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) → ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) ) |
16 |
14 15
|
rspcimdv |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( ∀ 𝑎 ∈ 𝐴 ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) → ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) ) |
17 |
|
vex |
⊢ 𝑚 ∈ V |
18 |
|
feq1 |
⊢ ( 𝑥 = 𝑚 → ( 𝑥 : { 𝑌 } ⟶ 𝐵 ↔ 𝑚 : { 𝑌 } ⟶ 𝐵 ) ) |
19 |
17 18 2
|
elab2 |
⊢ ( 𝑚 ∈ 𝐺 ↔ 𝑚 : { 𝑌 } ⟶ 𝐵 ) |
20 |
|
vex |
⊢ 𝑛 ∈ V |
21 |
|
feq1 |
⊢ ( 𝑥 = 𝑛 → ( 𝑥 : { 𝑌 } ⟶ 𝐵 ↔ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ) |
22 |
20 21 2
|
elab2 |
⊢ ( 𝑛 ∈ 𝐺 ↔ 𝑛 : { 𝑌 } ⟶ 𝐵 ) |
23 |
19 22
|
anbi12i |
⊢ ( ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ↔ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ) |
24 |
|
simp3 |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) → ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) |
25 |
|
simp1r |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) → 𝑌 ∈ 𝐴 ) |
26 |
|
fveq2 |
⊢ ( 𝑦 = 𝑌 → ( 𝑚 ‘ 𝑦 ) = ( 𝑚 ‘ 𝑌 ) ) |
27 |
|
fveq2 |
⊢ ( 𝑦 = 𝑌 → ( 𝑛 ‘ 𝑦 ) = ( 𝑛 ‘ 𝑌 ) ) |
28 |
26 27
|
eqeq12d |
⊢ ( 𝑦 = 𝑌 → ( ( 𝑚 ‘ 𝑦 ) = ( 𝑛 ‘ 𝑦 ) ↔ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) ) |
29 |
28
|
ralsng |
⊢ ( 𝑌 ∈ 𝐴 → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝑚 ‘ 𝑦 ) = ( 𝑛 ‘ 𝑦 ) ↔ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) ) |
30 |
25 29
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) → ( ∀ 𝑦 ∈ { 𝑌 } ( 𝑚 ‘ 𝑦 ) = ( 𝑛 ‘ 𝑦 ) ↔ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) ) |
31 |
24 30
|
mpbird |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) → ∀ 𝑦 ∈ { 𝑌 } ( 𝑚 ‘ 𝑦 ) = ( 𝑛 ‘ 𝑦 ) ) |
32 |
|
ffn |
⊢ ( 𝑚 : { 𝑌 } ⟶ 𝐵 → 𝑚 Fn { 𝑌 } ) |
33 |
|
ffn |
⊢ ( 𝑛 : { 𝑌 } ⟶ 𝐵 → 𝑛 Fn { 𝑌 } ) |
34 |
32 33
|
anim12i |
⊢ ( ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) → ( 𝑚 Fn { 𝑌 } ∧ 𝑛 Fn { 𝑌 } ) ) |
35 |
34
|
3ad2ant2 |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) → ( 𝑚 Fn { 𝑌 } ∧ 𝑛 Fn { 𝑌 } ) ) |
36 |
|
eqfnfv |
⊢ ( ( 𝑚 Fn { 𝑌 } ∧ 𝑛 Fn { 𝑌 } ) → ( 𝑚 = 𝑛 ↔ ∀ 𝑦 ∈ { 𝑌 } ( 𝑚 ‘ 𝑦 ) = ( 𝑛 ‘ 𝑦 ) ) ) |
37 |
35 36
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) → ( 𝑚 = 𝑛 ↔ ∀ 𝑦 ∈ { 𝑌 } ( 𝑚 ‘ 𝑦 ) = ( 𝑛 ‘ 𝑦 ) ) ) |
38 |
31 37
|
mpbird |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) ∧ ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) ) → 𝑚 = 𝑛 ) |
39 |
38
|
3exp |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑚 : { 𝑌 } ⟶ 𝐵 ∧ 𝑛 : { 𝑌 } ⟶ 𝐵 ) → ( ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) → 𝑚 = 𝑛 ) ) ) |
40 |
23 39
|
syl5bi |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) → ( ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) → 𝑚 = 𝑛 ) ) ) |
41 |
40
|
imp |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) → 𝑚 = 𝑛 ) ) |
42 |
16 41
|
syld |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( ∀ 𝑎 ∈ 𝐴 ( 𝑚 ‘ 𝑌 ) = ( 𝑛 ‘ 𝑌 ) → 𝑚 = 𝑛 ) ) |
43 |
13 42
|
sylbid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( ( 𝑎 ∈ 𝐴 ↦ ( 𝑚 ‘ 𝑌 ) ) = ( 𝑎 ∈ 𝐴 ↦ ( 𝑛 ‘ 𝑌 ) ) → 𝑚 = 𝑛 ) ) |
44 |
9 43
|
sylbid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) ∧ ( 𝑚 ∈ 𝐺 ∧ 𝑛 ∈ 𝐺 ) ) → ( ( 𝐻 ‘ 𝑚 ) = ( 𝐻 ‘ 𝑛 ) → 𝑚 = 𝑛 ) ) |
45 |
44
|
ralrimivva |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ∀ 𝑚 ∈ 𝐺 ∀ 𝑛 ∈ 𝐺 ( ( 𝐻 ‘ 𝑚 ) = ( 𝐻 ‘ 𝑛 ) → 𝑚 = 𝑛 ) ) |
46 |
|
dff13 |
⊢ ( 𝐻 : 𝐺 –1-1→ 𝐹 ↔ ( 𝐻 : 𝐺 ⟶ 𝐹 ∧ ∀ 𝑚 ∈ 𝐺 ∀ 𝑛 ∈ 𝐺 ( ( 𝐻 ‘ 𝑚 ) = ( 𝐻 ‘ 𝑛 ) → 𝑚 = 𝑛 ) ) ) |
47 |
4 45 46
|
sylanbrc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → 𝐻 : 𝐺 –1-1→ 𝐹 ) |