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 33257
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 2761 . . . . . . . . 9 (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) = (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
21elrnmpt 5940 . . . . . . . 8 (𝑧 ∈ V → (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})))
32elv 3456 . . . . . . 7 (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦}))
4 simpr 490 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 = (◡𝐹 “ {𝑦}))
5 simpl3 1212 . . . . . . . . . . . 12 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐵 ⊆ ran 𝐹)
6 simpr 490 . . . . . . . . . . . 12 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
75, 6sseldd 3932 . . . . . . . . . . 11 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ran 𝐹)
8 inisegn0 6096 . . . . . . . . . . 11 (𝑦 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑦}) ≠ ∅)
97, 8sylib 221 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ≠ ∅)
109adantr 486 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → (◡𝐹 “ {𝑦}) ≠ ∅)
114, 10eqnetrd 3023 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅)
1211r19.29an 3167 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅)
133, 12sylan2b 606 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝑧 ≠ ∅)
1413ralrimiva 3155 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ≠ ∅)
15 simp2 1155 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 Fn 𝐴)
16 simp1 1154 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐴 ∈ 𝑉)
1715, 16jca 521 . . . . . . . 8 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉))
18 fnex 7221 . . . . . . . 8 ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V)
19 rnexg 7912 . . . . . . . 8 (𝐹 ∈ V → ran 𝐹 ∈ V)
2017, 18, 193syl 19 . . . . . . 7 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ran 𝐹 ∈ V)
21 simp3 1156 . . . . . . 7 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ⊆ ran 𝐹)
2220, 21ssexd 5286 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ∈ V)
23 mptexg 7225 . . . . . 6 (𝐵 ∈ V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
24 rnexg 7912 . . . . . 6 ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
25 fvi 6959 . . . . . 6 (ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
2622, 23, 24, 254syl 20 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
2714, 26raleqtrrdv 3324 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅)
28 fvex 6896 . . . . 5 ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∈ V
2928ac5b 10549 . . . 4 (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅ → ∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧))
3027, 29syl 18 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧))
3126unieqd 4880 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
3226, 31feq23d 6702 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ↔ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))))
3326raleqdv 3320 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧 ↔ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))
3432, 33anbi12d 644 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)))
3534exbidv 1954 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)))
3630, 35mpbid 235 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))
37 vex 3455 . . . . . . . . 9 𝑓 ∈ V
3837rnex 7920 . . . . . . . 8 ran 𝑓 ∈ V
3938a1i 11 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ V)
40 simplr 781 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
41 frn 6715 . . . . . . . . 9 (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → ran 𝑓 ⊆ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
4240, 41syl 18 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
43 nfv 1947 . . . . . . . . . . . . 13 Ⅎ𝑦(𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹)
44 nfcv 2923 . . . . . . . . . . . . . 14 Ⅎ𝑦𝑓
45 nfmpt1 5204 . . . . . . . . . . . . . . 15 Ⅎ𝑦(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
4645nfrn 5934 . . . . . . . . . . . . . 14 Ⅎ𝑦ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
4746nfuni 4874 . . . . . . . . . . . . . 14 Ⅎ𝑦∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
4844, 46, 47nff 6703 . . . . . . . . . . . . 13 Ⅎ𝑦 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
4943, 48nfan 1932 . . . . . . . . . . . 12 Ⅎ𝑦((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
50 nfv 1947 . . . . . . . . . . . . 13 Ⅎ𝑦(𝑓‘𝑧) ∈ 𝑧
5146, 50nfralw 3310 . . . . . . . . . . . 12 Ⅎ𝑦∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧
5249, 51nfan 1932 . . . . . . . . . . 11 Ⅎ𝑦(((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)
5317, 18syl 18 . . . . . . . . . . . . . . 15 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 ∈ V)
5453ad3antrrr 743 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V)
55 cnvexg 7934 . . . . . . . . . . . . . 14 (𝐹 ∈ V → ◡𝐹 ∈ V)
56 imaexg 7923 . . . . . . . . . . . . . 14 (◡𝐹 ∈ V → (◡𝐹 “ {𝑦}) ∈ V)
5754, 55, 563syl 19 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V)
58 cnvimass 6197 . . . . . . . . . . . . . . 15 (◡𝐹 “ {𝑦}) ⊆ dom 𝐹
5958a1i 11 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ dom 𝐹)
6015fndmd 6642 . . . . . . . . . . . . . . 15 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → dom 𝐹 = 𝐴)
6160ad3antrrr 743 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → dom 𝐹 = 𝐴)
6259, 61sseqtrd 3967 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ 𝐴)
6357, 62elpwd 4563 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴)
6463ex 418 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴))
6552, 64ralrimi 3261 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴)
661rnmptss 7121 . . . . . . . . . 10 (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴 → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴)
6765, 66syl 18 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴)
68 sspwuni 5060 . . . . . . . . 9 (ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴 ↔ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴)
6967, 68sylib 221 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴)
7042, 69sstrd 3941 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ 𝐴)
7139, 70elpwd 4563 . . . . . 6 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ 𝒫 𝐴)
72 fnfun 6637 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn 𝐴 → Fun 𝐹)
7315, 72syl 18 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → Fun 𝐹)
7473ad5antr 747 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Fun 𝐹)
75 sndisj 5095 . . . . . . . . . . . . . . . . . . 19 Disj 𝑦 ∈ 𝐵 {𝑦}
76 disjpreima 33171 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ Disj 𝑦 ∈ 𝐵 {𝑦}) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}))
7774, 75, 76sylancl 598 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}))
78 disjrnmpt 33172 . . . . . . . . . . . . . . . . . 18 (Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧)
7977, 78syl 18 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧)
80 simpllr 788 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
81 simplr 781 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
82 simp-4r 796 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)
83 fveq2 6883 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢))
84 id 23 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → 𝑧 = 𝑢)
8583, 84eleq12d 2855 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
8685rspcv 3573 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑢) ∈ 𝑢))
8786imp 412 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑢) ∈ 𝑢)
8880, 82, 87syl2anc 596 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑢)
89 simpr 490 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) = (𝑓‘𝑣))
90 fveq2 6883 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑣 → (𝑓‘𝑧) = (𝑓‘𝑣))
91 id 23 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑣 → 𝑧 = 𝑣)
9290, 91eleq12d 2855 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑣 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑣) ∈ 𝑣))
9392rspcv 3573 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑣) ∈ 𝑣))
9493imp 412 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑣) ∈ 𝑣)
9581, 82, 94syl2anc 596 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑣) ∈ 𝑣)
9689, 95eqeltrd 2861 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑣)
9784, 91disji 5088 . . . . . . . . . . . . . . . . 17 ((Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ((𝑓‘𝑢) ∈ 𝑢 ∧ (𝑓‘𝑢) ∈ 𝑣)) → 𝑢 = 𝑣)
9879, 80, 81, 88, 96, 97syl122anc 1406 . . . . . . . . . . . . . . . 16 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 = 𝑣)
9998ex 418 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))
10099anasss 472 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))
101100ralrimivva 3206 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))
10240, 101jca 521 . . . . . . . . . . . 12 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)))
103 dff13 7256 . . . . . . . . . . . 12 (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)))
104102, 103sylibr 237 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
105 f1f1orn 6834 . . . . . . . . . . 11 (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran 𝑓)
106104, 105syl 18 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran 𝑓)
107 f1oen3g 8986 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran 𝑓) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓)
10837, 106, 107sylancr 599 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓)
109108ensymd 9025 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
11022, 23syl 18 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
111110ad2antrr 739 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
11257ex 418 . . . . . . . . . . . . . 14 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ V))
11352, 112ralrimi 3261 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V)
11473ad5antr 747 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → Fun 𝐹)
115 simpr 490 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ≠ 𝑡)
11621ad5antr 747 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝐵 ⊆ ran 𝐹)
117 simpllr 788 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ 𝐵)
118116, 117sseldd 3932 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ ran 𝐹)
119 simplr 781 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ 𝐵)
120116, 119sseldd 3932 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ ran 𝐹)
121114, 115, 118, 120preimane 33256 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡}))
122121ex 418 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (𝑦 ≠ 𝑡 → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡})))
123122necon4d 2980 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))
124123ralrimiva 3155 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))
125124ex 418 . . . . . . . . . . . . . 14 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)))
12652, 125ralrimi 3261 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))
127113, 126jca 521 . . . . . . . . . . . 12 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)))
128 sneq 4594 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → {𝑦} = {𝑡})
129128imaeq2d 6052 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}))
1301, 129f1mpt 7263 . . . . . . . . . . . 12 ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V ↔ (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)))
131127, 130sylibr 237 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V)
132 f1f1orn 6834 . . . . . . . . . . 11 ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
133131, 132syl 18 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
134 f1oen3g 8986 . . . . . . . . . 10 (((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V ∧ (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
135111, 133, 134syl2anc 596 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
136135ensymd 9025 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵)
137 entr 9026 . . . . . . . 8 ((ran 𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵) → ran 𝑓 ≈ 𝐵)
138109, 136, 137syl2anc 596 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ 𝐵)
139 imass2 6055 . . . . . . . . . . 11 (ran 𝑓 ⊆ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))))
14041, 139syl 18 . . . . . . . . . 10 (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))))
14140, 140syl 18 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))))
142 imauni 7248 . . . . . . . . . 10 (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧)
143 imaeq2 6048 . . . . . . . . . . . . 13 (𝑧 = (◡𝐹 “ {𝑦}) → (𝐹 “ 𝑧) = (𝐹 “ (◡𝐹 “ {𝑦})))
14453adantr 486 . . . . . . . . . . . . . 14 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V)
145144, 55, 563syl 19 . . . . . . . . . . . . 13 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V)
146143, 145iunrnmptss 33152 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ ∪ 𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})))
147 funimacnv 6619 . . . . . . . . . . . . . . . . 17 (Fun 𝐹 → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹))
14873, 147syl 18 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹))
149148adantr 486 . . . . . . . . . . . . . . 15 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹))
1506snssd 4747 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ 𝐵)
151150, 5sstrd 3941 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ ran 𝐹)
152 dfss2 3917 . . . . . . . . . . . . . . . 16 ({𝑦} ⊆ ran 𝐹 ↔ ({𝑦} ∩ ran 𝐹) = {𝑦})
153151, 152sylib 221 . . . . . . . . . . . . . . 15 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → ({𝑦} ∩ ran 𝐹) = {𝑦})
154149, 153eqtrd 2796 . . . . . . . . . . . . . 14 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = {𝑦})
155154iuneq2dv 4976 . . . . . . . . . . . . 13 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = ∪ 𝑦 ∈ 𝐵 {𝑦})
156 iunid 5019 . . . . . . . . . . . . 13 ∪ 𝑦 ∈ 𝐵 {𝑦} = 𝐵
157155, 156eqtrdi 2812 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = 𝐵)
158146, 157sseqtrd 3967 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵)
159158ad2antrr 739 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵)
160142, 159eqsstrid 3969 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ⊆ 𝐵)
161141, 160sstrd 3941 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) ⊆ 𝐵)
16240adantr 486 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
163162ffund 6712 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → Fun 𝑓)
164 simpr 490 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
16553, 55syl 18 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ◡𝐹 ∈ V)
166165ad3antrrr 743 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ◡𝐹 ∈ V)
167 imaexg 7923 . . . . . . . . . . . . . . . 16 (◡𝐹 ∈ V → (◡𝐹 “ {𝑡}) ∈ V)
168166, 167syl 18 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ V)
1691, 129elrnmpt1s 5941 . . . . . . . . . . . . . . 15 ((𝑡 ∈ 𝐵 ∧ (◡𝐹 “ {𝑡}) ∈ V) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
170164, 168, 169syl2anc 596 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
171162fdmd 6718 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → dom 𝑓 = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
172170, 171eleqtrrd 2864 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ dom 𝑓)
173 fvelrn 7074 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ (◡𝐹 “ {𝑡}) ∈ dom 𝑓) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓)
174163, 172, 173syl2anc 596 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓)
17515ad3antrrr 743 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝐹 Fn 𝐴)
176 simplr 781 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)
177 fveq2 6883 . . . . . . . . . . . . . . . . 17 (𝑧 = (◡𝐹 “ {𝑡}) → (𝑓‘𝑧) = (𝑓‘(◡𝐹 “ {𝑡})))
178 id 23 . . . . . . . . . . . . . . . . 17 (𝑧 = (◡𝐹 “ {𝑡}) → 𝑧 = (◡𝐹 “ {𝑡}))
179177, 178eleq12d 2855 . . . . . . . . . . . . . . . 16 (𝑧 = (◡𝐹 “ {𝑡}) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})))
180179rspcv 3573 . . . . . . . . . . . . . . 15 ((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})))
181180imp 412 . . . . . . . . . . . . . 14 (((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))
182170, 176, 181syl2anc 596 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))
183 fniniseg 7057 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → ((𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}) ↔ ((𝑓‘(◡𝐹 “ {𝑡})) ∈ 𝐴 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)))
184183simplbda 505 . . . . . . . . . . . . 13 ((𝐹 Fn 𝐴 ∧ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)
185175, 182, 184syl2anc 596 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)
186 fveqeq2 6892 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(◡𝐹 “ {𝑡})) → ((𝐹‘𝑘) = 𝑡 ↔ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡))
187186rspcev 3577 . . . . . . . . . . . 12 (((𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡)
188174, 185, 187syl2anc 596 . . . . . . . . . . 11 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡)
18970adantr 486 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ran 𝑓 ⊆ 𝐴)
190175, 189fvelimabd 6956 . . . . . . . . . . 11 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑡 ∈ (𝐹 “ ran 𝑓) ↔ ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡))
191188, 190mpbird 260 . . . . . . . . . 10 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝐹 “ ran 𝑓))
192191ex 418 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑡 ∈ 𝐵 → 𝑡 ∈ (𝐹 “ ran 𝑓)))
193192ssrdv 3937 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ⊆ (𝐹 “ ran 𝑓))
194161, 193eqssd 3948 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) = 𝐵)
195138, 194jca 521 . . . . . 6 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵))
196 breq1 5106 . . . . . . . 8 (𝑥 = ran 𝑓 → (𝑥 ≈ 𝐵 ↔ ran 𝑓 ≈ 𝐵))
197 imaeq2 6048 . . . . . . . . 9 (𝑥 = ran 𝑓 → (𝐹 “ 𝑥) = (𝐹 “ ran 𝑓))
198197eqeq1d 2763 . . . . . . . 8 (𝑥 = ran 𝑓 → ((𝐹 “ 𝑥) = 𝐵 ↔ (𝐹 “ ran 𝑓) = 𝐵))
199196, 198anbi12d 644 . . . . . . 7 (𝑥 = ran 𝑓 → ((𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵) ↔ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)))
200199rspcev 3577 . . . . . 6 ((ran 𝑓 ∈ 𝒫 𝐴 ∧ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
20171, 195, 200syl2anc 596 . . . . 5 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
202201anasss 472 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
203202ex 418 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)))
204203exlimdv 1966 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)))
20536, 204mpd 16 1 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
Colors of variables:    wff setvar class
This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ∪ cuni 4867  ∪ ciun 4951  Disj wdisj 5070   class class class wbr 5103   ↦ cmpt 5186   I cid 5545  ◡ccnv 5650  dom cdm 5651  ran crn 5652   “ cima 5654  Fun wfun 6531   Fn wfn 6532  ⟶wf 6533  –1-1→wf1 6534  –1-1-onto→wf1o 6536  ‘cfv 6537   ≈ cen 8963
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-ac2 10534
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-disj 5071  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-er 8710  df-en 8967  df-card 10013  df-ac 10188
This theorem is used by: (None)
  Copyright terms: Public domain W3C validator