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) Remove dependency on ax-reg and ax-inf2 . (Revised by Timothy J. O'Malley, 15-Oct-2026)

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

Proof

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