This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem foresf1o

Description: From a surjective function, *choose* a subset of the domain, such that the restricted function is bijective. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Assertion foresf1o ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝐹 ↾ 𝑥 ) : 𝑥 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 focdmex ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : 𝐴 –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 ffvelcdmda ⊢ ( ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : 𝐴 –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→ 𝐵 )