Metamath Proof Explorer


Theorem fnpreimac

Description: Choose a set x containing a preimage of each element of a given set B . (Contributed by Thierry Arnoux, 7-May-2023)

Ref Expression
Assertion fnpreimac ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqid ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) = ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) )
2 1 elrnmpt ( 𝑧 ∈ V → ( 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ↔ ∃ 𝑦𝐵 𝑧 = ( 𝐹 “ { 𝑦 } ) ) )
3 2 elv ( 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ↔ ∃ 𝑦𝐵 𝑧 = ( 𝐹 “ { 𝑦 } ) )
4 simpr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) ∧ 𝑧 = ( 𝐹 “ { 𝑦 } ) ) → 𝑧 = ( 𝐹 “ { 𝑦 } ) )
5 simpl3 ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → 𝐵 ⊆ ran 𝐹 )
6 simpr ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → 𝑦𝐵 )
7 5 6 sseldd ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → 𝑦 ∈ ran 𝐹 )
8 inisegn0 ( 𝑦 ∈ ran 𝐹 ↔ ( 𝐹 “ { 𝑦 } ) ≠ ∅ )
9 7 8 sylib ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ { 𝑦 } ) ≠ ∅ )
10 9 adantr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) ∧ 𝑧 = ( 𝐹 “ { 𝑦 } ) ) → ( 𝐹 “ { 𝑦 } ) ≠ ∅ )
11 4 10 eqnetrd ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) ∧ 𝑧 = ( 𝐹 “ { 𝑦 } ) ) → 𝑧 ≠ ∅ )
12 11 r19.29an ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ ∃ 𝑦𝐵 𝑧 = ( 𝐹 “ { 𝑦 } ) ) → 𝑧 ≠ ∅ )
13 3 12 sylan2b ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) → 𝑧 ≠ ∅ )
14 13 ralrimiva ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) 𝑧 ≠ ∅ )
15 simp2 ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝐹 Fn 𝐴 )
16 simp1 ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝐴𝑉 )
17 15 16 jca ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( 𝐹 Fn 𝐴𝐴𝑉 ) )
18 fnex ( ( 𝐹 Fn 𝐴𝐴𝑉 ) → 𝐹 ∈ V )
19 rnexg ( 𝐹 ∈ V → ran 𝐹 ∈ V )
20 17 18 19 3syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ran 𝐹 ∈ V )
21 simp3 ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝐵 ⊆ ran 𝐹 )
22 20 21 ssexd ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝐵 ∈ V )
23 mptexg ( 𝐵 ∈ V → ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V )
24 rnexg ( ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V )
25 22 23 24 3syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V )
26 fvi ( ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V → ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) = ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
27 25 26 syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) = ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
28 27 raleqdv ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) 𝑧 ≠ ∅ ↔ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) 𝑧 ≠ ∅ ) )
29 14 28 mpbird ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) 𝑧 ≠ ∅ )
30 fvex ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∈ V
31 30 ac5b ( ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) 𝑧 ≠ ∅ → ∃ 𝑓 ( 𝑓 : ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ⟶ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) )
32 29 31 syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ∃ 𝑓 ( 𝑓 : ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ⟶ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) )
33 27 unieqd ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) = ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
34 27 33 feq23d ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( 𝑓 : ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ⟶ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ↔ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) )
35 27 raleqdv ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ( 𝑓𝑧 ) ∈ 𝑧 ↔ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) )
36 34 35 anbi12d ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( ( 𝑓 : ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ⟶ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ↔ ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ) )
37 36 exbidv ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( ∃ 𝑓 ( 𝑓 : ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ⟶ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ( I ‘ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ↔ ∃ 𝑓 ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ) )
38 32 37 mpbid ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ∃ 𝑓 ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) )
39 vex 𝑓 ∈ V
40 39 rnex ran 𝑓 ∈ V
41 40 a1i ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran 𝑓 ∈ V )
42 simplr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
43 frn ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) → ran 𝑓 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
44 42 43 syl ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran 𝑓 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
45 nfv 𝑦 ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 )
46 nfcv 𝑦 𝑓
47 nfmpt1 𝑦 ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) )
48 47 nfrn 𝑦 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) )
49 48 nfuni 𝑦 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) )
50 46 48 49 nff 𝑦 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) )
51 45 50 nfan 𝑦 ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
52 nfv 𝑦 ( 𝑓𝑧 ) ∈ 𝑧
53 48 52 nfralw 𝑦𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧
54 51 53 nfan 𝑦 ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 )
55 17 18 syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝐹 ∈ V )
56 55 ad3antrrr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) → 𝐹 ∈ V )
57 cnvexg ( 𝐹 ∈ V → 𝐹 ∈ V )
58 imaexg ( 𝐹 ∈ V → ( 𝐹 “ { 𝑦 } ) ∈ V )
59 56 57 58 3syl ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ { 𝑦 } ) ∈ V )
60 cnvimass ( 𝐹 “ { 𝑦 } ) ⊆ dom 𝐹
61 60 a1i ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ { 𝑦 } ) ⊆ dom 𝐹 )
62 15 fndmd ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → dom 𝐹 = 𝐴 )
63 62 ad3antrrr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) → dom 𝐹 = 𝐴 )
64 61 63 sseqtrd ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ { 𝑦 } ) ⊆ 𝐴 )
65 59 64 elpwd ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ { 𝑦 } ) ∈ 𝒫 𝐴 )
66 65 ex ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑦𝐵 → ( 𝐹 “ { 𝑦 } ) ∈ 𝒫 𝐴 ) )
67 54 66 ralrimi ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) ∈ 𝒫 𝐴 )
68 1 rnmptss ( ∀ 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) ∈ 𝒫 𝐴 → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⊆ 𝒫 𝐴 )
69 67 68 syl ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⊆ 𝒫 𝐴 )
70 sspwuni ( ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⊆ 𝒫 𝐴 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⊆ 𝐴 )
71 69 70 sylib ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⊆ 𝐴 )
72 44 71 sstrd ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran 𝑓𝐴 )
73 41 72 elpwd ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran 𝑓 ∈ 𝒫 𝐴 )
74 fnfun ( 𝐹 Fn 𝐴 → Fun 𝐹 )
75 15 74 syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → Fun 𝐹 )
76 75 ad5antr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → Fun 𝐹 )
77 sndisj Disj 𝑦𝐵 { 𝑦 }
78 disjpreima ( ( Fun 𝐹Disj 𝑦𝐵 { 𝑦 } ) → Disj 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) )
79 76 77 78 sylancl ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → Disj 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) )
80 disjrnmpt ( Disj 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) → Disj 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) 𝑧 )
81 79 80 syl ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → Disj 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) 𝑧 )
82 simpllr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
83 simplr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
84 simp-4r ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 )
85 fveq2 ( 𝑧 = 𝑢 → ( 𝑓𝑧 ) = ( 𝑓𝑢 ) )
86 id ( 𝑧 = 𝑢𝑧 = 𝑢 )
87 85 86 eleq12d ( 𝑧 = 𝑢 → ( ( 𝑓𝑧 ) ∈ 𝑧 ↔ ( 𝑓𝑢 ) ∈ 𝑢 ) )
88 87 rspcv ( 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) → ( ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 → ( 𝑓𝑢 ) ∈ 𝑢 ) )
89 88 imp ( ( 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑓𝑢 ) ∈ 𝑢 )
90 82 84 89 syl2anc ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → ( 𝑓𝑢 ) ∈ 𝑢 )
91 simpr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → ( 𝑓𝑢 ) = ( 𝑓𝑣 ) )
92 fveq2 ( 𝑧 = 𝑣 → ( 𝑓𝑧 ) = ( 𝑓𝑣 ) )
93 id ( 𝑧 = 𝑣𝑧 = 𝑣 )
94 92 93 eleq12d ( 𝑧 = 𝑣 → ( ( 𝑓𝑧 ) ∈ 𝑧 ↔ ( 𝑓𝑣 ) ∈ 𝑣 ) )
95 94 rspcv ( 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) → ( ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 → ( 𝑓𝑣 ) ∈ 𝑣 ) )
96 95 imp ( ( 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑓𝑣 ) ∈ 𝑣 )
97 83 84 96 syl2anc ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → ( 𝑓𝑣 ) ∈ 𝑣 )
98 91 97 eqeltrd ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → ( 𝑓𝑢 ) ∈ 𝑣 )
99 86 93 disji ( ( Disj 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) 𝑧 ∧ ( 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( ( 𝑓𝑢 ) ∈ 𝑢 ∧ ( 𝑓𝑢 ) ∈ 𝑣 ) ) → 𝑢 = 𝑣 )
100 81 82 83 90 98 99 syl122anc ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ( 𝑓𝑢 ) = ( 𝑓𝑣 ) ) → 𝑢 = 𝑣 )
101 100 ex ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) → ( ( 𝑓𝑢 ) = ( 𝑓𝑣 ) → 𝑢 = 𝑣 ) )
102 101 anasss ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ ( 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ) → ( ( 𝑓𝑢 ) = ( 𝑓𝑣 ) → 𝑢 = 𝑣 ) )
103 102 ralrimivva ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∀ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( ( 𝑓𝑢 ) = ( 𝑓𝑣 ) → 𝑢 = 𝑣 ) )
104 42 103 jca ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∀ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( ( 𝑓𝑢 ) = ( 𝑓𝑣 ) → 𝑢 = 𝑣 ) ) )
105 dff13 ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) –1-1 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ↔ ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑢 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∀ 𝑣 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( ( 𝑓𝑢 ) = ( 𝑓𝑣 ) → 𝑢 = 𝑣 ) ) )
106 104 105 sylibr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) –1-1 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
107 f1f1orn ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) –1-1 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) → 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) –1-1-onto→ ran 𝑓 )
108 106 107 syl ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) –1-1-onto→ ran 𝑓 )
109 f1oen3g ( ( 𝑓 ∈ V ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) –1-1-onto→ ran 𝑓 ) → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ≈ ran 𝑓 )
110 39 108 109 sylancr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ≈ ran 𝑓 )
111 110 ensymd ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran 𝑓 ≈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
112 22 23 syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V )
113 112 ad2antrr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V )
114 59 ex ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑦𝐵 → ( 𝐹 “ { 𝑦 } ) ∈ V ) )
115 54 114 ralrimi ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) ∈ V )
116 75 ad5antr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → Fun 𝐹 )
117 simpr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → 𝑦𝑡 )
118 21 ad5antr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → 𝐵 ⊆ ran 𝐹 )
119 simpllr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → 𝑦𝐵 )
120 118 119 sseldd ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → 𝑦 ∈ ran 𝐹 )
121 simplr ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → 𝑡𝐵 )
122 118 121 sseldd ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → 𝑡 ∈ ran 𝐹 )
123 116 117 120 122 preimane ( ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) ∧ 𝑦𝑡 ) → ( 𝐹 “ { 𝑦 } ) ≠ ( 𝐹 “ { 𝑡 } ) )
124 123 ex ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) → ( 𝑦𝑡 → ( 𝐹 “ { 𝑦 } ) ≠ ( 𝐹 “ { 𝑡 } ) ) )
125 124 necon4d ( ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) ∧ 𝑡𝐵 ) → ( ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝑡 } ) → 𝑦 = 𝑡 ) )
126 125 ralrimiva ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑦𝐵 ) → ∀ 𝑡𝐵 ( ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝑡 } ) → 𝑦 = 𝑡 ) )
127 126 ex ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑦𝐵 → ∀ 𝑡𝐵 ( ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝑡 } ) → 𝑦 = 𝑡 ) ) )
128 54 127 ralrimi ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ∀ 𝑦𝐵𝑡𝐵 ( ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝑡 } ) → 𝑦 = 𝑡 ) )
129 115 128 jca ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ∀ 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) ∈ V ∧ ∀ 𝑦𝐵𝑡𝐵 ( ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝑡 } ) → 𝑦 = 𝑡 ) ) )
130 sneq ( 𝑦 = 𝑡 → { 𝑦 } = { 𝑡 } )
131 130 imaeq2d ( 𝑦 = 𝑡 → ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝑡 } ) )
132 1 131 f1mpt ( ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) : 𝐵1-1→ V ↔ ( ∀ 𝑦𝐵 ( 𝐹 “ { 𝑦 } ) ∈ V ∧ ∀ 𝑦𝐵𝑡𝐵 ( ( 𝐹 “ { 𝑦 } ) = ( 𝐹 “ { 𝑡 } ) → 𝑦 = 𝑡 ) ) )
133 129 132 sylibr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) : 𝐵1-1→ V )
134 f1f1orn ( ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) : 𝐵1-1→ V → ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) : 𝐵1-1-onto→ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
135 133 134 syl ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) : 𝐵1-1-onto→ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
136 f1oen3g ( ( ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∈ V ∧ ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) : 𝐵1-1-onto→ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) → 𝐵 ≈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
137 113 135 136 syl2anc ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → 𝐵 ≈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
138 137 ensymd ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ≈ 𝐵 )
139 entr ( ( ran 𝑓 ≈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ≈ 𝐵 ) → ran 𝑓𝐵 )
140 111 138 139 syl2anc ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ran 𝑓𝐵 )
141 imass2 ( ran 𝑓 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) → ( 𝐹 “ ran 𝑓 ) ⊆ ( 𝐹 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) )
142 43 141 syl ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) → ( 𝐹 “ ran 𝑓 ) ⊆ ( 𝐹 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) )
143 42 142 syl ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝐹 “ ran 𝑓 ) ⊆ ( 𝐹 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) )
144 imauni ( 𝐹 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) = 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝐹𝑧 )
145 imaeq2 ( 𝑧 = ( 𝐹 “ { 𝑦 } ) → ( 𝐹𝑧 ) = ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) )
146 55 adantr ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → 𝐹 ∈ V )
147 146 57 58 3syl ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ { 𝑦 } ) ∈ V )
148 145 147 iunrnmptss ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝐹𝑧 ) ⊆ 𝑦𝐵 ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) )
149 funimacnv ( Fun 𝐹 → ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) = ( { 𝑦 } ∩ ran 𝐹 ) )
150 75 149 syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) = ( { 𝑦 } ∩ ran 𝐹 ) )
151 150 adantr ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) = ( { 𝑦 } ∩ ran 𝐹 ) )
152 6 snssd ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → { 𝑦 } ⊆ 𝐵 )
153 152 5 sstrd ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → { 𝑦 } ⊆ ran 𝐹 )
154 df-ss ( { 𝑦 } ⊆ ran 𝐹 ↔ ( { 𝑦 } ∩ ran 𝐹 ) = { 𝑦 } )
155 153 154 sylib ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → ( { 𝑦 } ∩ ran 𝐹 ) = { 𝑦 } )
156 151 155 eqtrd ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑦𝐵 ) → ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) = { 𝑦 } )
157 156 iuneq2dv ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝑦𝐵 ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) = 𝑦𝐵 { 𝑦 } )
158 iunid 𝑦𝐵 { 𝑦 } = 𝐵
159 157 158 eqtrdi ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝑦𝐵 ( 𝐹 “ ( 𝐹 “ { 𝑦 } ) ) = 𝐵 )
160 148 159 sseqtrd ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝐹𝑧 ) ⊆ 𝐵 )
161 160 ad2antrr ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝐹𝑧 ) ⊆ 𝐵 )
162 144 161 eqsstrid ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝐹 ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ⊆ 𝐵 )
163 143 162 sstrd ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝐹 “ ran 𝑓 ) ⊆ 𝐵 )
164 42 adantr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
165 164 ffund ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → Fun 𝑓 )
166 simpr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → 𝑡𝐵 )
167 55 57 syl ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → 𝐹 ∈ V )
168 167 ad3antrrr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → 𝐹 ∈ V )
169 imaexg ( 𝐹 ∈ V → ( 𝐹 “ { 𝑡 } ) ∈ V )
170 168 169 syl ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ( 𝐹 “ { 𝑡 } ) ∈ V )
171 1 131 elrnmpt1s ( ( 𝑡𝐵 ∧ ( 𝐹 “ { 𝑡 } ) ∈ V ) → ( 𝐹 “ { 𝑡 } ) ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
172 166 170 171 syl2anc ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ( 𝐹 “ { 𝑡 } ) ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
173 164 fdmd ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → dom 𝑓 = ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) )
174 172 173 eleqtrrd ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ( 𝐹 “ { 𝑡 } ) ∈ dom 𝑓 )
175 fvelrn ( ( Fun 𝑓 ∧ ( 𝐹 “ { 𝑡 } ) ∈ dom 𝑓 ) → ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ran 𝑓 )
176 165 174 175 syl2anc ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ran 𝑓 )
177 15 ad3antrrr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → 𝐹 Fn 𝐴 )
178 simplr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 )
179 fveq2 ( 𝑧 = ( 𝐹 “ { 𝑡 } ) → ( 𝑓𝑧 ) = ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) )
180 id ( 𝑧 = ( 𝐹 “ { 𝑡 } ) → 𝑧 = ( 𝐹 “ { 𝑡 } ) )
181 179 180 eleq12d ( 𝑧 = ( 𝐹 “ { 𝑡 } ) → ( ( 𝑓𝑧 ) ∈ 𝑧 ↔ ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ( 𝐹 “ { 𝑡 } ) ) )
182 181 rspcv ( ( 𝐹 “ { 𝑡 } ) ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) → ( ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 → ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ( 𝐹 “ { 𝑡 } ) ) )
183 182 imp ( ( ( 𝐹 “ { 𝑡 } ) ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ( 𝐹 “ { 𝑡 } ) )
184 172 178 183 syl2anc ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ( 𝐹 “ { 𝑡 } ) )
185 fniniseg ( 𝐹 Fn 𝐴 → ( ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ( 𝐹 “ { 𝑡 } ) ↔ ( ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ 𝐴 ∧ ( 𝐹 ‘ ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ) = 𝑡 ) ) )
186 185 simplbda ( ( 𝐹 Fn 𝐴 ∧ ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ( 𝐹 “ { 𝑡 } ) ) → ( 𝐹 ‘ ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ) = 𝑡 )
187 177 184 186 syl2anc ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ( 𝐹 ‘ ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ) = 𝑡 )
188 fveqeq2 ( 𝑘 = ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) → ( ( 𝐹𝑘 ) = 𝑡 ↔ ( 𝐹 ‘ ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ) = 𝑡 ) )
189 188 rspcev ( ( ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ∈ ran 𝑓 ∧ ( 𝐹 ‘ ( 𝑓 ‘ ( 𝐹 “ { 𝑡 } ) ) ) = 𝑡 ) → ∃ 𝑘 ∈ ran 𝑓 ( 𝐹𝑘 ) = 𝑡 )
190 176 187 189 syl2anc ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ∃ 𝑘 ∈ ran 𝑓 ( 𝐹𝑘 ) = 𝑡 )
191 72 adantr ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ran 𝑓𝐴 )
192 177 191 fvelimabd ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → ( 𝑡 ∈ ( 𝐹 “ ran 𝑓 ) ↔ ∃ 𝑘 ∈ ran 𝑓 ( 𝐹𝑘 ) = 𝑡 ) )
193 190 192 mpbird ( ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ∧ 𝑡𝐵 ) → 𝑡 ∈ ( 𝐹 “ ran 𝑓 ) )
194 193 ex ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝑡𝐵𝑡 ∈ ( 𝐹 “ ran 𝑓 ) ) )
195 194 ssrdv ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → 𝐵 ⊆ ( 𝐹 “ ran 𝑓 ) )
196 163 195 eqssd ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( 𝐹 “ ran 𝑓 ) = 𝐵 )
197 140 196 jca ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ( ran 𝑓𝐵 ∧ ( 𝐹 “ ran 𝑓 ) = 𝐵 ) )
198 breq1 ( 𝑥 = ran 𝑓 → ( 𝑥𝐵 ↔ ran 𝑓𝐵 ) )
199 imaeq2 ( 𝑥 = ran 𝑓 → ( 𝐹𝑥 ) = ( 𝐹 “ ran 𝑓 ) )
200 199 eqeq1d ( 𝑥 = ran 𝑓 → ( ( 𝐹𝑥 ) = 𝐵 ↔ ( 𝐹 “ ran 𝑓 ) = 𝐵 ) )
201 198 200 anbi12d ( 𝑥 = ran 𝑓 → ( ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) ↔ ( ran 𝑓𝐵 ∧ ( 𝐹 “ ran 𝑓 ) = 𝐵 ) ) )
202 201 rspcev ( ( ran 𝑓 ∈ 𝒫 𝐴 ∧ ( ran 𝑓𝐵 ∧ ( 𝐹 “ ran 𝑓 ) = 𝐵 ) ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) )
203 73 197 202 syl2anc ( ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) )
204 203 anasss ( ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) ∧ ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) )
205 204 ex ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) ) )
206 205 exlimdv ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ( ∃ 𝑓 ( 𝑓 : ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ⟶ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ∧ ∀ 𝑧 ∈ ran ( 𝑦𝐵 ↦ ( 𝐹 “ { 𝑦 } ) ) ( 𝑓𝑧 ) ∈ 𝑧 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) ) )
207 38 206 mpd ( ( 𝐴𝑉𝐹 Fn 𝐴𝐵 ⊆ ran 𝐹 ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( 𝑥𝐵 ∧ ( 𝐹𝑥 ) = 𝐵 ) )