Step |
Hyp |
Ref |
Expression |
1 |
|
f1omptsn.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) |
2 |
|
f1omptsn.r |
⊢ 𝑅 = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } } |
3 |
|
eqid |
⊢ { 𝑥 } = { 𝑥 } |
4 |
|
snex |
⊢ { 𝑥 } ∈ V |
5 |
|
eqsbc3 |
⊢ ( { 𝑥 } ∈ V → ( [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ↔ { 𝑥 } = { 𝑥 } ) ) |
6 |
4 5
|
ax-mp |
⊢ ( [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ↔ { 𝑥 } = { 𝑥 } ) |
7 |
3 6
|
mpbir |
⊢ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } |
8 |
|
sbcel2 |
⊢ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 ) |
9 |
|
csbconstg |
⊢ ( { 𝑥 } ∈ V → ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 = 𝐴 ) |
10 |
4 9
|
ax-mp |
⊢ ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 = 𝐴 |
11 |
10
|
eleq2i |
⊢ ( 𝑥 ∈ ⦋ { 𝑥 } / 𝑢 ⦌ 𝐴 ↔ 𝑥 ∈ 𝐴 ) |
12 |
8 11
|
bitri |
⊢ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) |
13 |
2
|
abeq2i |
⊢ ( 𝑢 ∈ 𝑅 ↔ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } ) |
14 |
|
df-rex |
⊢ ( ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) ) |
15 |
13 14
|
sylbbr |
⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) |
16 |
15
|
19.23bi |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) |
17 |
16
|
sbcth |
⊢ ( { 𝑥 } ∈ V → [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) ) |
18 |
4 17
|
ax-mp |
⊢ [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) |
19 |
|
sbcimg |
⊢ ( { 𝑥 } ∈ V → ( [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) ↔ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 ) ) ) |
20 |
4 19
|
ax-mp |
⊢ ( [ { 𝑥 } / 𝑢 ] ( ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → 𝑢 ∈ 𝑅 ) ↔ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 ) ) |
21 |
18 20
|
mpbi |
⊢ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) → [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 ) |
22 |
|
sbcan |
⊢ ( [ { 𝑥 } / 𝑢 ] ( 𝑥 ∈ 𝐴 ∧ 𝑢 = { 𝑥 } ) ↔ ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) ) |
23 |
|
sbcel1v |
⊢ ( [ { 𝑥 } / 𝑢 ] 𝑢 ∈ 𝑅 ↔ { 𝑥 } ∈ 𝑅 ) |
24 |
21 22 23
|
3imtr3i |
⊢ ( ( [ { 𝑥 } / 𝑢 ] 𝑥 ∈ 𝐴 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) → { 𝑥 } ∈ 𝑅 ) |
25 |
12 24
|
sylanbr |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ [ { 𝑥 } / 𝑢 ] 𝑢 = { 𝑥 } ) → { 𝑥 } ∈ 𝑅 ) |
26 |
7 25
|
mpan2 |
⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ∈ 𝑅 ) |
27 |
1 26
|
fmpti |
⊢ 𝐹 : 𝐴 ⟶ 𝑅 |
28 |
1
|
fvmpt2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ { 𝑥 } ∈ 𝑅 ) → ( 𝐹 ‘ 𝑥 ) = { 𝑥 } ) |
29 |
26 28
|
mpdan |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) = { 𝑥 } ) |
30 |
|
sneq |
⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } ) |
31 |
30 1 4
|
fvmpt3i |
⊢ ( 𝑦 ∈ 𝐴 → ( 𝐹 ‘ 𝑦 ) = { 𝑦 } ) |
32 |
29 31
|
eqeqan12d |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ { 𝑥 } = { 𝑦 } ) ) |
33 |
|
vex |
⊢ 𝑥 ∈ V |
34 |
|
sneqbg |
⊢ ( 𝑥 ∈ V → ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) ) |
35 |
33 34
|
ax-mp |
⊢ ( { 𝑥 } = { 𝑦 } ↔ 𝑥 = 𝑦 ) |
36 |
32 35
|
syl6bb |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) ) |
37 |
36
|
biimpd |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) |
38 |
37
|
rgen2 |
⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) |
39 |
|
dff13 |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝑅 ↔ ( 𝐹 : 𝐴 ⟶ 𝑅 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ) |
40 |
27 38 39
|
mpbir2an |
⊢ 𝐹 : 𝐴 –1-1→ 𝑅 |
41 |
|
f1f1orn |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝑅 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ) |
42 |
40 41
|
ax-mp |
⊢ 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 |
43 |
|
rnmptsn |
⊢ ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) = { 𝑢 ∣ ∃ 𝑥 ∈ 𝐴 𝑢 = { 𝑥 } } |
44 |
1
|
rneqi |
⊢ ran 𝐹 = ran ( 𝑥 ∈ 𝐴 ↦ { 𝑥 } ) |
45 |
43 44 2
|
3eqtr4i |
⊢ ran 𝐹 = 𝑅 |
46 |
|
f1oeq3 |
⊢ ( ran 𝐹 = 𝑅 → ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝑅 ) ) |
47 |
45 46
|
ax-mp |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ↔ 𝐹 : 𝐴 –1-1-onto→ 𝑅 ) |
48 |
42 47
|
mpbi |
⊢ 𝐹 : 𝐴 –1-1-onto→ 𝑅 |