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

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