Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnpreimac Structured version   Visualization version   GIF version
Theorem fnpreimac 32164
Description: Choose a set π‘₯ containing a preimage of each element of a given set 𝐡. (Contributed by Thierry Arnoux, 7-May-2023.)
Assertion
Ref Expression
fnpreimac ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐡   π‘₯,𝐹
Allowed substitution hint:   𝑉(π‘₯)
Proof of Theorem fnpreimac
Dummy variables 𝑓 𝑑 𝑒 𝑣 𝑦 𝑧 π‘˜ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2731 . . . . . . . . 9 (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) = (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))
21elrnmpt 5955 . . . . . . . 8 (𝑧 ∈ V β†’ (𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ↔ βˆƒπ‘¦ ∈ 𝐡 𝑧 = (◑𝐹 β€œ {𝑦})))
32elv 3479 . . . . . . 7 (𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ↔ βˆƒπ‘¦ ∈ 𝐡 𝑧 = (◑𝐹 β€œ {𝑦}))
4 simpr 484 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 = (◑𝐹 β€œ {𝑦})) β†’ 𝑧 = (◑𝐹 β€œ {𝑦}))
5 simpl3 1192 . . . . . . . . . . . 12 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ 𝐡 βŠ† ran 𝐹)
6 simpr 484 . . . . . . . . . . . 12 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 ∈ 𝐡)
75, 6sseldd 3983 . . . . . . . . . . 11 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ 𝑦 ∈ ran 𝐹)
8 inisegn0 6097 . . . . . . . . . . 11 (𝑦 ∈ ran 𝐹 ↔ (◑𝐹 β€œ {𝑦}) β‰  βˆ…)
97, 8sylib 217 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑦}) β‰  βˆ…)
109adantr 480 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 = (◑𝐹 β€œ {𝑦})) β†’ (◑𝐹 β€œ {𝑦}) β‰  βˆ…)
114, 10eqnetrd 3007 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) ∧ 𝑧 = (◑𝐹 β€œ {𝑦})) β†’ 𝑧 β‰  βˆ…)
1211r19.29an 3157 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ βˆƒπ‘¦ ∈ 𝐡 𝑧 = (◑𝐹 β€œ {𝑦})) β†’ 𝑧 β‰  βˆ…)
133, 12sylan2b 593 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) β†’ 𝑧 β‰  βˆ…)
1413ralrimiva 3145 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))𝑧 β‰  βˆ…)
15 simp2 1136 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ 𝐹 Fn 𝐴)
16 simp1 1135 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ 𝐴 ∈ 𝑉)
1715, 16jca 511 . . . . . . . . . 10 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉))
18 fnex 7221 . . . . . . . . . 10 ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) β†’ 𝐹 ∈ V)
19 rnexg 7899 . . . . . . . . . 10 (𝐹 ∈ V β†’ ran 𝐹 ∈ V)
2017, 18, 193syl 18 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ ran 𝐹 ∈ V)
21 simp3 1137 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ 𝐡 βŠ† ran 𝐹)
2220, 21ssexd 5324 . . . . . . . 8 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ 𝐡 ∈ V)
23 mptexg 7225 . . . . . . . 8 (𝐡 ∈ V β†’ (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V)
24 rnexg 7899 . . . . . . . 8 ((𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V β†’ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V)
2522, 23, 243syl 18 . . . . . . 7 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V)
26 fvi 6967 . . . . . . 7 (ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V β†’ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) = ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
2725, 26syl 17 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) = ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
2827raleqdv 3324 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))𝑧 β‰  βˆ… ↔ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))𝑧 β‰  βˆ…))
2914, 28mpbird 257 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))𝑧 β‰  βˆ…)
30 fvex 6904 . . . . 5 ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∈ V
3130ac5b 10477 . . . 4 (βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))𝑧 β‰  βˆ… β†’ βˆƒπ‘“(𝑓:( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))⟢βˆͺ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))(π‘“β€˜π‘§) ∈ 𝑧))
3229, 31syl 17 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆƒπ‘“(𝑓:( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))⟢βˆͺ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))(π‘“β€˜π‘§) ∈ 𝑧))
3327unieqd 4922 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆͺ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) = βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
3427, 33feq23d 6712 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (𝑓:( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))⟢βˆͺ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ↔ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))))
3527raleqdv 3324 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))(π‘“β€˜π‘§) ∈ 𝑧 ↔ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧))
3634, 35anbi12d 630 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ ((𝑓:( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))⟢βˆͺ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))(π‘“β€˜π‘§) ∈ 𝑧) ↔ (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧)))
3736exbidv 1923 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (βˆƒπ‘“(𝑓:( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))⟢βˆͺ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ( I β€˜ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))(π‘“β€˜π‘§) ∈ 𝑧) ↔ βˆƒπ‘“(𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧)))
3832, 37mpbid 231 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆƒπ‘“(𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧))
39 vex 3477 . . . . . . . . 9 𝑓 ∈ V
4039rnex 7907 . . . . . . . 8 ran 𝑓 ∈ V
4140a1i 11 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran 𝑓 ∈ V)
42 simplr 766 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
43 frn 6724 . . . . . . . . 9 (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β†’ ran 𝑓 βŠ† βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
4442, 43syl 17 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran 𝑓 βŠ† βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
45 nfv 1916 . . . . . . . . . . . . 13 Ⅎ𝑦(𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹)
46 nfcv 2902 . . . . . . . . . . . . . 14 Ⅎ𝑦𝑓
47 nfmpt1 5256 . . . . . . . . . . . . . . 15 Ⅎ𝑦(𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))
4847nfrn 5951 . . . . . . . . . . . . . 14 Ⅎ𝑦ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))
4948nfuni 4915 . . . . . . . . . . . . . 14 Ⅎ𝑦βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))
5046, 48, 49nff 6713 . . . . . . . . . . . . 13 Ⅎ𝑦 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))
5145, 50nfan 1901 . . . . . . . . . . . 12 Ⅎ𝑦((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
52 nfv 1916 . . . . . . . . . . . . 13 Ⅎ𝑦(π‘“β€˜π‘§) ∈ 𝑧
5348, 52nfralw 3307 . . . . . . . . . . . 12 β„²π‘¦βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧
5451, 53nfan 1901 . . . . . . . . . . 11 Ⅎ𝑦(((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧)
5517, 18syl 17 . . . . . . . . . . . . . . 15 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ 𝐹 ∈ V)
5655ad3antrrr 727 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) β†’ 𝐹 ∈ V)
57 cnvexg 7919 . . . . . . . . . . . . . 14 (𝐹 ∈ V β†’ ◑𝐹 ∈ V)
58 imaexg 7910 . . . . . . . . . . . . . 14 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ {𝑦}) ∈ V)
5956, 57, 583syl 18 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑦}) ∈ V)
60 cnvimass 6080 . . . . . . . . . . . . . . 15 (◑𝐹 β€œ {𝑦}) βŠ† dom 𝐹
6160a1i 11 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑦}) βŠ† dom 𝐹)
6215fndmd 6654 . . . . . . . . . . . . . . 15 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ dom 𝐹 = 𝐴)
6362ad3antrrr 727 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) β†’ dom 𝐹 = 𝐴)
6461, 63sseqtrd 4022 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑦}) βŠ† 𝐴)
6559, 64elpwd 4608 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑦}) ∈ 𝒫 𝐴)
6665ex 412 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑦 ∈ 𝐡 β†’ (◑𝐹 β€œ {𝑦}) ∈ 𝒫 𝐴))
6754, 66ralrimi 3253 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆ€π‘¦ ∈ 𝐡 (◑𝐹 β€œ {𝑦}) ∈ 𝒫 𝐴)
681rnmptss 7124 . . . . . . . . . 10 (βˆ€π‘¦ ∈ 𝐡 (◑𝐹 β€œ {𝑦}) ∈ 𝒫 𝐴 β†’ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) βŠ† 𝒫 𝐴)
6967, 68syl 17 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) βŠ† 𝒫 𝐴)
70 sspwuni 5103 . . . . . . . . 9 (ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) βŠ† 𝒫 𝐴 ↔ βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) βŠ† 𝐴)
7169, 70sylib 217 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) βŠ† 𝐴)
7244, 71sstrd 3992 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran 𝑓 βŠ† 𝐴)
7341, 72elpwd 4608 . . . . . 6 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran 𝑓 ∈ 𝒫 𝐴)
74 fnfun 6649 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn 𝐴 β†’ Fun 𝐹)
7515, 74syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ Fun 𝐹)
7675ad5antr 731 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ Fun 𝐹)
77 sndisj 5139 . . . . . . . . . . . . . . . . . . 19 Disj 𝑦 ∈ 𝐡 {𝑦}
78 disjpreima 32083 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ Disj 𝑦 ∈ 𝐡 {𝑦}) β†’ Disj 𝑦 ∈ 𝐡 (◑𝐹 β€œ {𝑦}))
7976, 77, 78sylancl 585 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ Disj 𝑦 ∈ 𝐡 (◑𝐹 β€œ {𝑦}))
80 disjrnmpt 32084 . . . . . . . . . . . . . . . . . 18 (Disj 𝑦 ∈ 𝐡 (◑𝐹 β€œ {𝑦}) β†’ Disj 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))𝑧)
8179, 80syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ Disj 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))𝑧)
82 simpllr 773 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
83 simplr 766 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
84 simp-4r 781 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧)
85 fveq2 6891 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑒 β†’ (π‘“β€˜π‘§) = (π‘“β€˜π‘’))
86 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑒 β†’ 𝑧 = 𝑒)
8785, 86eleq12d 2826 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑒 β†’ ((π‘“β€˜π‘§) ∈ 𝑧 ↔ (π‘“β€˜π‘’) ∈ 𝑒))
8887rspcv 3608 . . . . . . . . . . . . . . . . . . 19 (𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β†’ (βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧 β†’ (π‘“β€˜π‘’) ∈ 𝑒))
8988imp 406 . . . . . . . . . . . . . . . . . 18 ((𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (π‘“β€˜π‘’) ∈ 𝑒)
9082, 84, 89syl2anc 583 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ (π‘“β€˜π‘’) ∈ 𝑒)
91 simpr 484 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ (π‘“β€˜π‘’) = (π‘“β€˜π‘£))
92 fveq2 6891 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑣 β†’ (π‘“β€˜π‘§) = (π‘“β€˜π‘£))
93 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑣 β†’ 𝑧 = 𝑣)
9492, 93eleq12d 2826 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑣 β†’ ((π‘“β€˜π‘§) ∈ 𝑧 ↔ (π‘“β€˜π‘£) ∈ 𝑣))
9594rspcv 3608 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β†’ (βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧 β†’ (π‘“β€˜π‘£) ∈ 𝑣))
9695imp 406 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (π‘“β€˜π‘£) ∈ 𝑣)
9783, 84, 96syl2anc 583 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ (π‘“β€˜π‘£) ∈ 𝑣)
9891, 97eqeltrd 2832 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ (π‘“β€˜π‘’) ∈ 𝑣)
9986, 93disji 5131 . . . . . . . . . . . . . . . . 17 ((Disj 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))𝑧 ∧ (𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ ((π‘“β€˜π‘’) ∈ 𝑒 ∧ (π‘“β€˜π‘’) ∈ 𝑣)) β†’ 𝑒 = 𝑣)
10081, 82, 83, 90, 98, 99syl122anc 1378 . . . . . . . . . . . . . . . 16 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ (π‘“β€˜π‘’) = (π‘“β€˜π‘£)) β†’ 𝑒 = 𝑣)
101100ex 412 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) β†’ ((π‘“β€˜π‘’) = (π‘“β€˜π‘£) β†’ 𝑒 = 𝑣))
102101anasss 466 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ (𝑒 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))) β†’ ((π‘“β€˜π‘’) = (π‘“β€˜π‘£) β†’ 𝑒 = 𝑣))
103102ralrimivva 3199 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆ€π‘’ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))βˆ€π‘£ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))((π‘“β€˜π‘’) = (π‘“β€˜π‘£) β†’ 𝑒 = 𝑣))
10442, 103jca 511 . . . . . . . . . . . 12 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘’ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))βˆ€π‘£ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))((π‘“β€˜π‘’) = (π‘“β€˜π‘£) β†’ 𝑒 = 𝑣)))
105 dff13 7257 . . . . . . . . . . . 12 (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))–1-1β†’βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ↔ (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘’ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))βˆ€π‘£ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))((π‘“β€˜π‘’) = (π‘“β€˜π‘£) β†’ 𝑒 = 𝑣)))
106104, 105sylibr 233 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))–1-1β†’βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
107 f1f1orn 6844 . . . . . . . . . . 11 (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))–1-1β†’βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β†’ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))–1-1-ontoβ†’ran 𝑓)
108106, 107syl 17 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))–1-1-ontoβ†’ran 𝑓)
109 f1oen3g 8966 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))–1-1-ontoβ†’ran 𝑓) β†’ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β‰ˆ ran 𝑓)
11039, 108, 109sylancr 586 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β‰ˆ ran 𝑓)
111110ensymd 9005 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran 𝑓 β‰ˆ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
11222, 23syl 17 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V)
113112ad2antrr 723 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V)
11459ex 412 . . . . . . . . . . . . . 14 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑦 ∈ 𝐡 β†’ (◑𝐹 β€œ {𝑦}) ∈ V))
11554, 114ralrimi 3253 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆ€π‘¦ ∈ 𝐡 (◑𝐹 β€œ {𝑦}) ∈ V)
11675ad5antr 731 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ Fun 𝐹)
117 simpr 484 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ 𝑦 β‰  𝑑)
11821ad5antr 731 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ 𝐡 βŠ† ran 𝐹)
119 simpllr 773 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ 𝑦 ∈ 𝐡)
120118, 119sseldd 3983 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ 𝑦 ∈ ran 𝐹)
121 simplr 766 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ 𝑑 ∈ 𝐡)
122118, 121sseldd 3983 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ 𝑑 ∈ ran 𝐹)
123116, 117, 120, 122preimane 32163 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) ∧ 𝑦 β‰  𝑑) β†’ (◑𝐹 β€œ {𝑦}) β‰  (◑𝐹 β€œ {𝑑}))
124123ex 412 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ (𝑦 β‰  𝑑 β†’ (◑𝐹 β€œ {𝑦}) β‰  (◑𝐹 β€œ {𝑑})))
125124necon4d 2963 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) ∧ 𝑑 ∈ 𝐡) β†’ ((◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑑}) β†’ 𝑦 = 𝑑))
126125ralrimiva 3145 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑦 ∈ 𝐡) β†’ βˆ€π‘‘ ∈ 𝐡 ((◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑑}) β†’ 𝑦 = 𝑑))
127126ex 412 . . . . . . . . . . . . . 14 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑦 ∈ 𝐡 β†’ βˆ€π‘‘ ∈ 𝐡 ((◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑑}) β†’ 𝑦 = 𝑑)))
12854, 127ralrimi 3253 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘‘ ∈ 𝐡 ((◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑑}) β†’ 𝑦 = 𝑑))
129115, 128jca 511 . . . . . . . . . . . 12 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (βˆ€π‘¦ ∈ 𝐡 (◑𝐹 β€œ {𝑦}) ∈ V ∧ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘‘ ∈ 𝐡 ((◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑑}) β†’ 𝑦 = 𝑑)))
130 sneq 4638 . . . . . . . . . . . . . 14 (𝑦 = 𝑑 β†’ {𝑦} = {𝑑})
131130imaeq2d 6059 . . . . . . . . . . . . 13 (𝑦 = 𝑑 β†’ (◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑑}))
1321, 131f1mpt 7263 . . . . . . . . . . . 12 ((𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})):𝐡–1-1β†’V ↔ (βˆ€π‘¦ ∈ 𝐡 (◑𝐹 β€œ {𝑦}) ∈ V ∧ βˆ€π‘¦ ∈ 𝐡 βˆ€π‘‘ ∈ 𝐡 ((◑𝐹 β€œ {𝑦}) = (◑𝐹 β€œ {𝑑}) β†’ 𝑦 = 𝑑)))
133129, 132sylibr 233 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})):𝐡–1-1β†’V)
134 f1f1orn 6844 . . . . . . . . . . 11 ((𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})):𝐡–1-1β†’V β†’ (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})):𝐡–1-1-ontoβ†’ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
135133, 134syl 17 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})):𝐡–1-1-ontoβ†’ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
136 f1oen3g 8966 . . . . . . . . . 10 (((𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∈ V ∧ (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})):𝐡–1-1-ontoβ†’ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) β†’ 𝐡 β‰ˆ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
137113, 135, 136syl2anc 583 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ 𝐡 β‰ˆ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
138137ensymd 9005 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β‰ˆ 𝐡)
139 entr 9006 . . . . . . . 8 ((ran 𝑓 β‰ˆ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β‰ˆ 𝐡) β†’ ran 𝑓 β‰ˆ 𝐡)
140111, 138, 139syl2anc 583 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ ran 𝑓 β‰ˆ 𝐡)
141 imass2 6101 . . . . . . . . . . 11 (ran 𝑓 βŠ† βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β†’ (𝐹 β€œ ran 𝑓) βŠ† (𝐹 β€œ βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))))
14243, 141syl 17 . . . . . . . . . 10 (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β†’ (𝐹 β€œ ran 𝑓) βŠ† (𝐹 β€œ βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))))
14342, 142syl 17 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝐹 β€œ ran 𝑓) βŠ† (𝐹 β€œ βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))))
144 imauni 7248 . . . . . . . . . 10 (𝐹 β€œ βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) = βˆͺ 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(𝐹 β€œ 𝑧)
145 imaeq2 6055 . . . . . . . . . . . . 13 (𝑧 = (◑𝐹 β€œ {𝑦}) β†’ (𝐹 β€œ 𝑧) = (𝐹 β€œ (◑𝐹 β€œ {𝑦})))
14655adantr 480 . . . . . . . . . . . . . 14 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ 𝐹 ∈ V)
147146, 57, 583syl 18 . . . . . . . . . . . . 13 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑦}) ∈ V)
148145, 147iunrnmptss 32065 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆͺ 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(𝐹 β€œ 𝑧) βŠ† βˆͺ 𝑦 ∈ 𝐡 (𝐹 β€œ (◑𝐹 β€œ {𝑦})))
149 funimacnv 6629 . . . . . . . . . . . . . . . . 17 (Fun 𝐹 β†’ (𝐹 β€œ (◑𝐹 β€œ {𝑦})) = ({𝑦} ∩ ran 𝐹))
15075, 149syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (𝐹 β€œ (◑𝐹 β€œ {𝑦})) = ({𝑦} ∩ ran 𝐹))
151150adantr 480 . . . . . . . . . . . . . . 15 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ (𝐹 β€œ (◑𝐹 β€œ {𝑦})) = ({𝑦} ∩ ran 𝐹))
1526snssd 4812 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ {𝑦} βŠ† 𝐡)
153152, 5sstrd 3992 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ {𝑦} βŠ† ran 𝐹)
154 df-ss 3965 . . . . . . . . . . . . . . . 16 ({𝑦} βŠ† ran 𝐹 ↔ ({𝑦} ∩ ran 𝐹) = {𝑦})
155153, 154sylib 217 . . . . . . . . . . . . . . 15 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ ({𝑦} ∩ ran 𝐹) = {𝑦})
156151, 155eqtrd 2771 . . . . . . . . . . . . . 14 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑦 ∈ 𝐡) β†’ (𝐹 β€œ (◑𝐹 β€œ {𝑦})) = {𝑦})
157156iuneq2dv 5021 . . . . . . . . . . . . 13 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆͺ 𝑦 ∈ 𝐡 (𝐹 β€œ (◑𝐹 β€œ {𝑦})) = βˆͺ 𝑦 ∈ 𝐡 {𝑦})
158 iunid 5063 . . . . . . . . . . . . 13 βˆͺ 𝑦 ∈ 𝐡 {𝑦} = 𝐡
159157, 158eqtrdi 2787 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆͺ 𝑦 ∈ 𝐡 (𝐹 β€œ (◑𝐹 β€œ {𝑦})) = 𝐡)
160148, 159sseqtrd 4022 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆͺ 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(𝐹 β€œ 𝑧) βŠ† 𝐡)
161160ad2antrr 723 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆͺ 𝑧 ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(𝐹 β€œ 𝑧) βŠ† 𝐡)
162144, 161eqsstrid 4030 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝐹 β€œ βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) βŠ† 𝐡)
163143, 162sstrd 3992 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝐹 β€œ ran 𝑓) βŠ† 𝐡)
16442adantr 480 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
165164ffund 6721 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ Fun 𝑓)
166 simpr 484 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ 𝑑 ∈ 𝐡)
16755, 57syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ ◑𝐹 ∈ V)
168167ad3antrrr 727 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ ◑𝐹 ∈ V)
169 imaexg 7910 . . . . . . . . . . . . . . . 16 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ {𝑑}) ∈ V)
170168, 169syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑑}) ∈ V)
1711, 131elrnmpt1s 5956 . . . . . . . . . . . . . . 15 ((𝑑 ∈ 𝐡 ∧ (◑𝐹 β€œ {𝑑}) ∈ V) β†’ (◑𝐹 β€œ {𝑑}) ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
172166, 170, 171syl2anc 583 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑑}) ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
173164fdmd 6728 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ dom 𝑓 = ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})))
174172, 173eleqtrrd 2835 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ (◑𝐹 β€œ {𝑑}) ∈ dom 𝑓)
175 fvelrn 7078 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ (◑𝐹 β€œ {𝑑}) ∈ dom 𝑓) β†’ (π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ ran 𝑓)
176165, 174, 175syl2anc 583 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ (π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ ran 𝑓)
17715ad3antrrr 727 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ 𝐹 Fn 𝐴)
178 simplr 766 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧)
179 fveq2 6891 . . . . . . . . . . . . . . . . 17 (𝑧 = (◑𝐹 β€œ {𝑑}) β†’ (π‘“β€˜π‘§) = (π‘“β€˜(◑𝐹 β€œ {𝑑})))
180 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 = (◑𝐹 β€œ {𝑑}) β†’ 𝑧 = (◑𝐹 β€œ {𝑑}))
181179, 180eleq12d 2826 . . . . . . . . . . . . . . . 16 (𝑧 = (◑𝐹 β€œ {𝑑}) β†’ ((π‘“β€˜π‘§) ∈ 𝑧 ↔ (π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ (◑𝐹 β€œ {𝑑})))
182181rspcv 3608 . . . . . . . . . . . . . . 15 ((◑𝐹 β€œ {𝑑}) ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) β†’ (βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧 β†’ (π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ (◑𝐹 β€œ {𝑑})))
183182imp 406 . . . . . . . . . . . . . 14 (((◑𝐹 β€œ {𝑑}) ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ (◑𝐹 β€œ {𝑑}))
184172, 178, 183syl2anc 583 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ (π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ (◑𝐹 β€œ {𝑑}))
185 fniniseg 7061 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 β†’ ((π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ (◑𝐹 β€œ {𝑑}) ↔ ((π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ 𝐴 ∧ (πΉβ€˜(π‘“β€˜(◑𝐹 β€œ {𝑑}))) = 𝑑)))
186185simplbda 499 . . . . . . . . . . . . 13 ((𝐹 Fn 𝐴 ∧ (π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ (◑𝐹 β€œ {𝑑})) β†’ (πΉβ€˜(π‘“β€˜(◑𝐹 β€œ {𝑑}))) = 𝑑)
187177, 184, 186syl2anc 583 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ (πΉβ€˜(π‘“β€˜(◑𝐹 β€œ {𝑑}))) = 𝑑)
188 fveqeq2 6900 . . . . . . . . . . . . 13 (π‘˜ = (π‘“β€˜(◑𝐹 β€œ {𝑑})) β†’ ((πΉβ€˜π‘˜) = 𝑑 ↔ (πΉβ€˜(π‘“β€˜(◑𝐹 β€œ {𝑑}))) = 𝑑))
189188rspcev 3612 . . . . . . . . . . . 12 (((π‘“β€˜(◑𝐹 β€œ {𝑑})) ∈ ran 𝑓 ∧ (πΉβ€˜(π‘“β€˜(◑𝐹 β€œ {𝑑}))) = 𝑑) β†’ βˆƒπ‘˜ ∈ ran 𝑓(πΉβ€˜π‘˜) = 𝑑)
190176, 187, 189syl2anc 583 . . . . . . . . . . 11 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ βˆƒπ‘˜ ∈ ran 𝑓(πΉβ€˜π‘˜) = 𝑑)
19172adantr 480 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ ran 𝑓 βŠ† 𝐴)
192177, 191fvelimabd 6965 . . . . . . . . . . 11 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ (𝑑 ∈ (𝐹 β€œ ran 𝑓) ↔ βˆƒπ‘˜ ∈ ran 𝑓(πΉβ€˜π‘˜) = 𝑑))
193190, 192mpbird 257 . . . . . . . . . 10 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) ∧ 𝑑 ∈ 𝐡) β†’ 𝑑 ∈ (𝐹 β€œ ran 𝑓))
194193ex 412 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝑑 ∈ 𝐡 β†’ 𝑑 ∈ (𝐹 β€œ ran 𝑓)))
195194ssrdv 3988 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ 𝐡 βŠ† (𝐹 β€œ ran 𝑓))
196163, 195eqssd 3999 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (𝐹 β€œ ran 𝑓) = 𝐡)
197140, 196jca 511 . . . . . 6 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ (ran 𝑓 β‰ˆ 𝐡 ∧ (𝐹 β€œ ran 𝑓) = 𝐡))
198 breq1 5151 . . . . . . . 8 (π‘₯ = ran 𝑓 β†’ (π‘₯ β‰ˆ 𝐡 ↔ ran 𝑓 β‰ˆ 𝐡))
199 imaeq2 6055 . . . . . . . . 9 (π‘₯ = ran 𝑓 β†’ (𝐹 β€œ π‘₯) = (𝐹 β€œ ran 𝑓))
200199eqeq1d 2733 . . . . . . . 8 (π‘₯ = ran 𝑓 β†’ ((𝐹 β€œ π‘₯) = 𝐡 ↔ (𝐹 β€œ ran 𝑓) = 𝐡))
201198, 200anbi12d 630 . . . . . . 7 (π‘₯ = ran 𝑓 β†’ ((π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡) ↔ (ran 𝑓 β‰ˆ 𝐡 ∧ (𝐹 β€œ ran 𝑓) = 𝐡)))
202201rspcev 3612 . . . . . 6 ((ran 𝑓 ∈ 𝒫 𝐴 ∧ (ran 𝑓 β‰ˆ 𝐡 ∧ (𝐹 β€œ ran 𝑓) = 𝐡)) β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡))
20373, 197, 202syl2anc 583 . . . . 5 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡))
204203anasss 466 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) ∧ (𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧)) β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡))
205204ex 412 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ ((𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡)))
206205exlimdv 1935 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ (βˆƒπ‘“(𝑓:ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))⟢βˆͺ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦})) ∧ βˆ€π‘§ ∈ ran (𝑦 ∈ 𝐡 ↦ (◑𝐹 β€œ {𝑦}))(π‘“β€˜π‘§) ∈ 𝑧) β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡)))
20738, 206mpd 15 1 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐡 βŠ† ran 𝐹) β†’ βˆƒπ‘₯ ∈ 𝒫 𝐴(π‘₯ β‰ˆ 𝐡 ∧ (𝐹 β€œ π‘₯) = 𝐡))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540  βˆƒwex 1780   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  βˆƒwrex 3069  Vcvv 3473   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  π’« cpw 4602  {csn 4628  βˆͺ cuni 4908  βˆͺ ciun 4997  Disj wdisj 5113   class class class wbr 5148   ↦ cmpt 5231   I cid 5573  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β€œ cima 5679  Fun wfun 6537   Fn wfn 6538  βŸΆwf 6539  β€“1-1β†’wf1 6540  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543   β‰ˆ cen 8940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-ac2 10462
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-disj 5114  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-er 8707  df-en 8944  df-card 9938  df-ac 10115
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator