Step |
Hyp |
Ref |
Expression |
1 |
|
fornex |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) ) |
2 |
1
|
imp |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ V ) |
3 |
|
foelrn |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) ) |
4 |
|
fofn |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 ) |
5 |
|
eqcom |
⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) |
6 |
|
fniniseg |
⊢ ( 𝐹 Fn 𝐴 → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) ) |
7 |
6
|
biimpar |
⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
8 |
7
|
anassrs |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) → 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
9 |
5 8
|
sylan2br |
⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
10 |
4 9
|
sylanl1 |
⊢ ( ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑧 ) ) → 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
11 |
10
|
ex |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑧 ) → 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) |
12 |
11
|
reximdva |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) → ∃ 𝑧 ∈ 𝐴 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑧 ∈ 𝐴 𝑦 = ( 𝐹 ‘ 𝑧 ) → ∃ 𝑧 ∈ 𝐴 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) |
14 |
3 13
|
mpd |
⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
15 |
14
|
adantll |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
16 |
15
|
ralrimiva |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
17 |
|
eleq1 |
⊢ ( 𝑧 = ( 𝑔 ‘ 𝑦 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) |
18 |
17
|
ac6sg |
⊢ ( 𝐵 ∈ V → ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐴 𝑧 ∈ ( ◡ 𝐹 “ { 𝑦 } ) → ∃ 𝑔 ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ) |
19 |
2 16 18
|
sylc |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ∃ 𝑔 ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) |
20 |
|
frn |
⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 → ran 𝑔 ⊆ 𝐴 ) |
21 |
20
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ran 𝑔 ⊆ 𝐴 ) |
22 |
|
vex |
⊢ 𝑔 ∈ V |
23 |
22
|
rnex |
⊢ ran 𝑔 ∈ V |
24 |
23
|
elpw |
⊢ ( ran 𝑔 ∈ 𝒫 𝐴 ↔ ran 𝑔 ⊆ 𝐴 ) |
25 |
21 24
|
sylibr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ran 𝑔 ∈ 𝒫 𝐴 ) |
26 |
|
fof |
⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
27 |
26
|
ad2antlr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
28 |
27 21
|
fssresd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ( 𝐹 ↾ ran 𝑔 ) : ran 𝑔 ⟶ 𝐵 ) |
29 |
|
ffn |
⊢ ( 𝑔 : 𝐵 ⟶ 𝐴 → 𝑔 Fn 𝐵 ) |
30 |
29
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → 𝑔 Fn 𝐵 ) |
31 |
|
dffn3 |
⊢ ( 𝑔 Fn 𝐵 ↔ 𝑔 : 𝐵 ⟶ ran 𝑔 ) |
32 |
30 31
|
sylib |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → 𝑔 : 𝐵 ⟶ ran 𝑔 ) |
33 |
|
fvres |
⊢ ( 𝑧 ∈ ran 𝑔 → ( ( 𝐹 ↾ ran 𝑔 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ) |
34 |
33
|
adantl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) → ( ( 𝐹 ↾ ran 𝑔 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) ) |
35 |
34
|
fveq2d |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) → ( 𝑔 ‘ ( ( 𝐹 ↾ ran 𝑔 ) ‘ 𝑧 ) ) = ( 𝑔 ‘ ( 𝐹 ‘ 𝑧 ) ) ) |
36 |
|
nfv |
⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) |
37 |
|
nfv |
⊢ Ⅎ 𝑦 𝑔 : 𝐵 ⟶ 𝐴 |
38 |
|
nfra1 |
⊢ Ⅎ 𝑦 ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) |
39 |
37 38
|
nfan |
⊢ Ⅎ 𝑦 ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
40 |
36 39
|
nfan |
⊢ Ⅎ 𝑦 ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) |
41 |
|
nfv |
⊢ Ⅎ 𝑦 𝑧 ∈ ran 𝑔 |
42 |
40 41
|
nfan |
⊢ Ⅎ 𝑦 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) |
43 |
|
simpr |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ( 𝑔 ‘ 𝑦 ) = 𝑧 ) |
44 |
43
|
fveq2d |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐹 ‘ 𝑧 ) ) |
45 |
4
|
ad5antlr |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → 𝐹 Fn 𝐴 ) |
46 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
47 |
46
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
48 |
|
simplr |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → 𝑦 ∈ 𝐵 ) |
49 |
|
rspa |
⊢ ( ( ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
50 |
47 48 49
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
51 |
|
fniniseg |
⊢ ( 𝐹 Fn 𝐴 → ( ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ↔ ( ( 𝑔 ‘ 𝑦 ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) = 𝑦 ) ) ) |
52 |
51
|
simplbda |
⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) → ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) = 𝑦 ) |
53 |
45 50 52
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) = 𝑦 ) |
54 |
44 53
|
eqtr3d |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ( 𝐹 ‘ 𝑧 ) = 𝑦 ) |
55 |
54
|
fveq2d |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ( 𝑔 ‘ ( 𝐹 ‘ 𝑧 ) ) = ( 𝑔 ‘ 𝑦 ) ) |
56 |
55 43
|
eqtrd |
⊢ ( ( ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑔 ‘ 𝑦 ) = 𝑧 ) → ( 𝑔 ‘ ( 𝐹 ‘ 𝑧 ) ) = 𝑧 ) |
57 |
|
fvelrnb |
⊢ ( 𝑔 Fn 𝐵 → ( 𝑧 ∈ ran 𝑔 ↔ ∃ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) = 𝑧 ) ) |
58 |
57
|
biimpa |
⊢ ( ( 𝑔 Fn 𝐵 ∧ 𝑧 ∈ ran 𝑔 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) = 𝑧 ) |
59 |
30 58
|
sylan |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) → ∃ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) = 𝑧 ) |
60 |
42 56 59
|
r19.29af |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) → ( 𝑔 ‘ ( 𝐹 ‘ 𝑧 ) ) = 𝑧 ) |
61 |
35 60
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑧 ∈ ran 𝑔 ) → ( 𝑔 ‘ ( ( 𝐹 ↾ ran 𝑔 ) ‘ 𝑧 ) ) = 𝑧 ) |
62 |
61
|
ralrimiva |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ∀ 𝑧 ∈ ran 𝑔 ( 𝑔 ‘ ( ( 𝐹 ↾ ran 𝑔 ) ‘ 𝑧 ) ) = 𝑧 ) |
63 |
32
|
ffvelrnda |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ‘ 𝑦 ) ∈ ran 𝑔 ) |
64 |
|
fvres |
⊢ ( ( 𝑔 ‘ 𝑦 ) ∈ ran 𝑔 → ( ( 𝐹 ↾ ran 𝑔 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) ) |
65 |
63 64
|
syl |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ↾ ran 𝑔 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) ) |
66 |
4
|
ad3antlr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐹 Fn 𝐴 ) |
67 |
|
simplrr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
68 |
|
simpr |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 ) |
69 |
67 68 49
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) |
70 |
66 69 52
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑔 ‘ 𝑦 ) ) = 𝑦 ) |
71 |
65 70
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐹 ↾ ran 𝑔 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = 𝑦 ) |
72 |
71
|
ex |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ( 𝑦 ∈ 𝐵 → ( ( 𝐹 ↾ ran 𝑔 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = 𝑦 ) ) |
73 |
40 72
|
ralrimi |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ↾ ran 𝑔 ) ‘ ( 𝑔 ‘ 𝑦 ) ) = 𝑦 ) |
74 |
28 32 62 73
|
2fvidf1od |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ( 𝐹 ↾ ran 𝑔 ) : ran 𝑔 –1-1-onto→ 𝐵 ) |
75 |
|
reseq2 |
⊢ ( 𝑥 = ran 𝑔 → ( 𝐹 ↾ 𝑥 ) = ( 𝐹 ↾ ran 𝑔 ) ) |
76 |
|
id |
⊢ ( 𝑥 = ran 𝑔 → 𝑥 = ran 𝑔 ) |
77 |
|
eqidd |
⊢ ( 𝑥 = ran 𝑔 → 𝐵 = 𝐵 ) |
78 |
75 76 77
|
f1oeq123d |
⊢ ( 𝑥 = ran 𝑔 → ( ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐵 ↔ ( 𝐹 ↾ ran 𝑔 ) : ran 𝑔 –1-1-onto→ 𝐵 ) ) |
79 |
78
|
rspcev |
⊢ ( ( ran 𝑔 ∈ 𝒫 𝐴 ∧ ( 𝐹 ↾ ran 𝑔 ) : ran 𝑔 –1-1-onto→ 𝐵 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐵 ) |
80 |
25 74 79
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) ∧ ( 𝑔 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑔 ‘ 𝑦 ) ∈ ( ◡ 𝐹 “ { 𝑦 } ) ) ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐵 ) |
81 |
19 80
|
exlimddv |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐵 ) |