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 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𝐵 )