Step |
Hyp |
Ref |
Expression |
1 |
|
1arymaptfv.h |
⊢ 𝐻 = ( ℎ ∈ ( 1 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
2 |
1
|
1arymaptf |
⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m 𝑋 ) ) |
3 |
1
|
1arymaptfv |
⊢ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) → ( 𝐻 ‘ 𝑓 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
4 |
3
|
ad2antrl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( 𝐻 ‘ 𝑓 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
5 |
1
|
1arymaptfv |
⊢ ( 𝑔 ∈ ( 1 -aryF 𝑋 ) → ( 𝐻 ‘ 𝑔 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
6 |
5
|
ad2antll |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( 𝐻 ‘ 𝑔 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
7 |
4 6
|
eqeq12d |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) ↔ ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ) ) |
8 |
|
fvex |
⊢ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ∈ V |
9 |
8
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ∈ V |
10 |
|
mpteqb |
⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ∈ V → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
11 |
9 10
|
mp1i |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ) |
12 |
|
1aryfvalel |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ↔ 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ) |
13 |
|
1aryfvalel |
⊢ ( 𝑋 ∈ 𝑉 → ( 𝑔 ∈ ( 1 -aryF 𝑋 ) ↔ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ) |
14 |
12 13
|
anbi12d |
⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ↔ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ) ) |
15 |
|
ffn |
⊢ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 → 𝑓 Fn ( 𝑋 ↑m { 0 } ) ) |
16 |
15
|
adantr |
⊢ ( ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) → 𝑓 Fn ( 𝑋 ↑m { 0 } ) ) |
17 |
16
|
3ad2ant2 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → 𝑓 Fn ( 𝑋 ↑m { 0 } ) ) |
18 |
|
ffn |
⊢ ( 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 → 𝑔 Fn ( 𝑋 ↑m { 0 } ) ) |
19 |
18
|
adantl |
⊢ ( ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) → 𝑔 Fn ( 𝑋 ↑m { 0 } ) ) |
20 |
19
|
3ad2ant2 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → 𝑔 Fn ( 𝑋 ↑m { 0 } ) ) |
21 |
|
elmapi |
⊢ ( 𝑦 ∈ ( 𝑋 ↑m { 0 } ) → 𝑦 : { 0 } ⟶ 𝑋 ) |
22 |
|
c0ex |
⊢ 0 ∈ V |
23 |
22
|
fsn2 |
⊢ ( 𝑦 : { 0 } ⟶ 𝑋 ↔ ( ( 𝑦 ‘ 0 ) ∈ 𝑋 ∧ 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) |
24 |
21 23
|
sylib |
⊢ ( 𝑦 ∈ ( 𝑋 ↑m { 0 } ) → ( ( 𝑦 ‘ 0 ) ∈ 𝑋 ∧ 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) |
25 |
|
opeq2 |
⊢ ( 𝑥 = ( 𝑦 ‘ 0 ) → 〈 0 , 𝑥 〉 = 〈 0 , ( 𝑦 ‘ 0 ) 〉 ) |
26 |
25
|
sneqd |
⊢ ( 𝑥 = ( 𝑦 ‘ 0 ) → { 〈 0 , 𝑥 〉 } = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) |
27 |
26
|
fveq2d |
⊢ ( 𝑥 = ( 𝑦 ‘ 0 ) → ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) |
28 |
26
|
fveq2d |
⊢ ( 𝑥 = ( 𝑦 ‘ 0 ) → ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) |
29 |
27 28
|
eqeq12d |
⊢ ( 𝑥 = ( 𝑦 ‘ 0 ) → ( ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ↔ ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) ) |
30 |
29
|
rspccv |
⊢ ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) → ( ( 𝑦 ‘ 0 ) ∈ 𝑋 → ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) ) |
31 |
30
|
3ad2ant3 |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → ( ( 𝑦 ‘ 0 ) ∈ 𝑋 → ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) ) |
32 |
31
|
com12 |
⊢ ( ( 𝑦 ‘ 0 ) ∈ 𝑋 → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) ) |
33 |
32
|
adantr |
⊢ ( ( ( 𝑦 ‘ 0 ) ∈ 𝑋 ∧ 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) ) |
34 |
|
fveq2 |
⊢ ( 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } → ( 𝑓 ‘ 𝑦 ) = ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) |
35 |
|
fveq2 |
⊢ ( 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) |
36 |
34 35
|
eqeq12d |
⊢ ( 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) ) |
37 |
36
|
adantl |
⊢ ( ( ( 𝑦 ‘ 0 ) ∈ 𝑋 ∧ 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ↔ ( 𝑓 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) = ( 𝑔 ‘ { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) ) ) |
38 |
33 37
|
sylibrd |
⊢ ( ( ( 𝑦 ‘ 0 ) ∈ 𝑋 ∧ 𝑦 = { 〈 0 , ( 𝑦 ‘ 0 ) 〉 } ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) ) |
39 |
24 38
|
syl |
⊢ ( 𝑦 ∈ ( 𝑋 ↑m { 0 } ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) ) |
40 |
39
|
impcom |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) ∧ 𝑦 ∈ ( 𝑋 ↑m { 0 } ) ) → ( 𝑓 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑦 ) ) |
41 |
17 20 40
|
eqfnfvd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → 𝑓 = 𝑔 ) |
42 |
41
|
3exp |
⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑓 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ∧ 𝑔 : ( 𝑋 ↑m { 0 } ) ⟶ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) → 𝑓 = 𝑔 ) ) ) |
43 |
14 42
|
sylbid |
⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) → 𝑓 = 𝑔 ) ) ) |
44 |
43
|
imp |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) = ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) → 𝑓 = 𝑔 ) ) |
45 |
11 44
|
sylbid |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝑥 ∈ 𝑋 ↦ ( 𝑓 ‘ { 〈 0 , 𝑥 〉 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝑔 ‘ { 〈 0 , 𝑥 〉 } ) ) → 𝑓 = 𝑔 ) ) |
46 |
7 45
|
sylbid |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑓 ∈ ( 1 -aryF 𝑋 ) ∧ 𝑔 ∈ ( 1 -aryF 𝑋 ) ) ) → ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) |
47 |
46
|
ralrimivva |
⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑓 ∈ ( 1 -aryF 𝑋 ) ∀ 𝑔 ∈ ( 1 -aryF 𝑋 ) ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) |
48 |
|
dff13 |
⊢ ( 𝐻 : ( 1 -aryF 𝑋 ) –1-1→ ( 𝑋 ↑m 𝑋 ) ↔ ( 𝐻 : ( 1 -aryF 𝑋 ) ⟶ ( 𝑋 ↑m 𝑋 ) ∧ ∀ 𝑓 ∈ ( 1 -aryF 𝑋 ) ∀ 𝑔 ∈ ( 1 -aryF 𝑋 ) ( ( 𝐻 ‘ 𝑓 ) = ( 𝐻 ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) ) |
49 |
2 47 48
|
sylanbrc |
⊢ ( 𝑋 ∈ 𝑉 → 𝐻 : ( 1 -aryF 𝑋 ) –1-1→ ( 𝑋 ↑m 𝑋 ) ) |