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 30434
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 2798 . . . . . . . . 9 (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) = (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
21elrnmpt 5792 . . . . . . . 8 (𝑧 ∈ V → (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})))
32elv 3446 . . . . . . 7 (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦}))
4 simpr 488 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 = (◡𝐹 “ {𝑦}))
5 simpl3 1190 . . . . . . . . . . . 12 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐵 ⊆ ran 𝐹)
6 simpr 488 . . . . . . . . . . . 12 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵)
75, 6sseldd 3916 . . . . . . . . . . 11 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ran 𝐹)
8 inisegn0 5928 . . . . . . . . . . 11 (𝑦 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑦}) ≠ ∅)
97, 8sylib 221 . . . . . . . . . 10 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ≠ ∅)
109adantr 484 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → (◡𝐹 “ {𝑦}) ≠ ∅)
114, 10eqnetrd 3054 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅)
1211r19.29an 3247 . . . . . . 7 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅)
133, 12sylan2b 596 . . . . . 6 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝑧 ≠ ∅)
1413ralrimiva 3149 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ≠ ∅)
15 simp2 1134 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 Fn 𝐴)
16 simp1 1133 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐴 ∈ 𝑉)
1715, 16jca 515 . . . . . . . . . 10 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉))
18 fnex 6957 . . . . . . . . . 10 ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V)
19 rnexg 7595 . . . . . . . . . 10 (𝐹 ∈ V → ran 𝐹 ∈ V)
2017, 18, 193syl 18 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ran 𝐹 ∈ V)
21 simp3 1135 . . . . . . . . 9 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ⊆ ran 𝐹)
2220, 21ssexd 5192 . . . . . . . 8 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ∈ V)
23 mptexg 6961 . . . . . . . 8 (𝐵 ∈ V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
24 rnexg 7595 . . . . . . . 8 ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
2522, 23, 243syl 18 . . . . . . 7 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
26 fvi 6715 . . . . . . 7 (ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
2725, 26syl 17 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
2827raleqdv 3364 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅ ↔ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ≠ ∅))
2914, 28mpbird 260 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅)
30 fvex 6658 . . . . 5 ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∈ V
3130ac5b 9889 . . . 4 (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅ → ∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧))
3229, 31syl 17 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧))
3327unieqd 4814 . . . . . 6 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
3427, 33feq23d 6482 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ↔ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))))
3527raleqdv 3364 . . . . 5 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧 ↔ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))
3634, 35anbi12d 633 . . . 4 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)))
3736exbidv 1922 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)))
3832, 37mpbid 235 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))
39 vex 3444 . . . . . . . . 9 𝑓 ∈ V
4039rnex 7599 . . . . . . . 8 ran 𝑓 ∈ V
4140a1i 11 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ V)
42 simplr 768 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
43 frn 6493 . . . . . . . . 9 (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → ran 𝑓 ⊆ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
4442, 43syl 17 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
45 nfv 1915 . . . . . . . . . . . . 13 Ⅎ𝑦(𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹)
46 nfcv 2955 . . . . . . . . . . . . . 14 Ⅎ𝑦𝑓
47 nfmpt1 5128 . . . . . . . . . . . . . . 15 Ⅎ𝑦(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
4847nfrn 5788 . . . . . . . . . . . . . 14 Ⅎ𝑦ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
4948nfuni 4807 . . . . . . . . . . . . . 14 Ⅎ𝑦∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
5046, 48, 49nff 6483 . . . . . . . . . . . . 13 Ⅎ𝑦 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))
5145, 50nfan 1900 . . . . . . . . . . . 12 Ⅎ𝑦((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
52 nfv 1915 . . . . . . . . . . . . 13 Ⅎ𝑦(𝑓‘𝑧) ∈ 𝑧
5348, 52nfralw 3189 . . . . . . . . . . . 12 Ⅎ𝑦∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧
5451, 53nfan 1900 . . . . . . . . . . 11 Ⅎ𝑦(((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)
5517, 18syl 17 . . . . . . . . . . . . . . 15 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 ∈ V)
5655ad3antrrr 729 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V)
57 cnvexg 7611 . . . . . . . . . . . . . 14 (𝐹 ∈ V → ◡𝐹 ∈ V)
58 imaexg 7602 . . . . . . . . . . . . . 14 (◡𝐹 ∈ V → (◡𝐹 “ {𝑦}) ∈ V)
5956, 57, 583syl 18 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V)
60 cnvimass 5916 . . . . . . . . . . . . . . 15 (◡𝐹 “ {𝑦}) ⊆ dom 𝐹
6160a1i 11 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ dom 𝐹)
6215fndmd 6427 . . . . . . . . . . . . . . 15 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → dom 𝐹 = 𝐴)
6362ad3antrrr 729 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → dom 𝐹 = 𝐴)
6461, 63sseqtrd 3955 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ 𝐴)
6559, 64elpwd 4505 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴)
6665ex 416 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴))
6754, 66ralrimi 3180 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴)
681rnmptss 6863 . . . . . . . . . 10 (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴 → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴)
6967, 68syl 17 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴)
70 sspwuni 4985 . . . . . . . . 9 (ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴 ↔ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴)
7169, 70sylib 221 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴)
7244, 71sstrd 3925 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ 𝐴)
7341, 72elpwd 4505 . . . . . 6 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ 𝒫 𝐴)
74 fnfun 6423 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn 𝐴 → Fun 𝐹)
7515, 74syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → Fun 𝐹)
7675ad5antr 733 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Fun 𝐹)
77 sndisj 5021 . . . . . . . . . . . . . . . . . . 19 Disj 𝑦 ∈ 𝐵 {𝑦}
78 disjpreima 30347 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹 ∧ Disj 𝑦 ∈ 𝐵 {𝑦}) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}))
7976, 77, 78sylancl 589 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}))
80 disjrnmpt 30348 . . . . . . . . . . . . . . . . . 18 (Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧)
8179, 80syl 17 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧)
82 simpllr 775 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
83 simplr 768 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
84 simp-4r 783 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)
85 fveq2 6645 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢))
86 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑢 → 𝑧 = 𝑢)
8785, 86eleq12d 2884 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢))
8887rspcv 3566 . . . . . . . . . . . . . . . . . . 19 (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑢) ∈ 𝑢))
8988imp 410 . . . . . . . . . . . . . . . . . 18 ((𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑢) ∈ 𝑢)
9082, 84, 89syl2anc 587 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑢)
91 simpr 488 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) = (𝑓‘𝑣))
92 fveq2 6645 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑣 → (𝑓‘𝑧) = (𝑓‘𝑣))
93 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑣 → 𝑧 = 𝑣)
9492, 93eleq12d 2884 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑣 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑣) ∈ 𝑣))
9594rspcv 3566 . . . . . . . . . . . . . . . . . . . 20 (𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑣) ∈ 𝑣))
9695imp 410 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑣) ∈ 𝑣)
9783, 84, 96syl2anc 587 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑣) ∈ 𝑣)
9891, 97eqeltrd 2890 . . . . . . . . . . . . . . . . 17 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑣)
9986, 93disji 5013 . . . . . . . . . . . . . . . . 17 ((Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ((𝑓‘𝑢) ∈ 𝑢 ∧ (𝑓‘𝑢) ∈ 𝑣)) → 𝑢 = 𝑣)
10081, 82, 83, 90, 98, 99syl122anc 1376 . . . . . . . . . . . . . . . 16 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 = 𝑣)
101100ex 416 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))
102101anasss 470 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))
103102ralrimivva 3156 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))
10442, 103jca 515 . . . . . . . . . . . 12 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)))
105 dff13 6991 . . . . . . . . . . . 12 (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)))
106104, 105sylibr 237 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
107 f1f1orn 6601 . . . . . . . . . . 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 8508 . . . . . . . . . 10 ((𝑓 ∈ V ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran 𝑓) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓)
11039, 108, 109sylancr 590 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓)
111110ensymd 8543 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
11222, 23syl 17 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
113112ad2antrr 725 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V)
11459ex 416 . . . . . . . . . . . . . 14 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ V))
11554, 114ralrimi 3180 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V)
11675ad5antr 733 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → Fun 𝐹)
117 simpr 488 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ≠ 𝑡)
11821ad5antr 733 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝐵 ⊆ ran 𝐹)
119 simpllr 775 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ 𝐵)
120118, 119sseldd 3916 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ ran 𝐹)
121 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ 𝐵)
122118, 121sseldd 3916 . . . . . . . . . . . . . . . . . . 19 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ ran 𝐹)
123116, 117, 120, 122preimane 30433 . . . . . . . . . . . . . . . . . 18 (((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡}))
124123ex 416 . . . . . . . . . . . . . . . . 17 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (𝑦 ≠ 𝑡 → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡})))
125124necon4d 3011 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))
126125ralrimiva 3149 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))
127126ex 416 . . . . . . . . . . . . . 14 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)))
12854, 127ralrimi 3180 . . . . . . . . . . . . 13 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))
129115, 128jca 515 . . . . . . . . . . . 12 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)))
130 sneq 4535 . . . . . . . . . . . . . 14 (𝑦 = 𝑡 → {𝑦} = {𝑡})
131130imaeq2d 5896 . . . . . . . . . . . . 13 (𝑦 = 𝑡 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}))
1321, 131f1mpt 6997 . . . . . . . . . . . 12 ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V ↔ (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)))
133129, 132sylibr 237 . . . . . . . . . . 11 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V)
134 f1f1orn 6601 . . . . . . . . . . 11 ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
135133, 134syl 17 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
136 f1oen3g 8508 . . . . . . . . . 10 (((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V ∧ (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
137113, 135, 136syl2anc 587 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
138137ensymd 8543 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵)
139 entr 8544 . . . . . . . 8 ((ran 𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵) → ran 𝑓 ≈ 𝐵)
140111, 138, 139syl2anc 587 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ 𝐵)
141 imass2 5932 . . . . . . . . . . 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 6983 . . . . . . . . . 10 (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧)
145 imaeq2 5892 . . . . . . . . . . . . 13 (𝑧 = (◡𝐹 “ {𝑦}) → (𝐹 “ 𝑧) = (𝐹 “ (◡𝐹 “ {𝑦})))
14655adantr 484 . . . . . . . . . . . . . 14 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V)
147146, 57, 583syl 18 . . . . . . . . . . . . 13 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V)
148145, 147iunrnmptss 30329 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ ∪ 𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})))
149 funimacnv 6405 . . . . . . . . . . . . . . . . 17 (Fun 𝐹 → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹))
15075, 149syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹))
151150adantr 484 . . . . . . . . . . . . . . 15 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹))
1526snssd 4702 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ 𝐵)
153152, 5sstrd 3925 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ ran 𝐹)
154 df-ss 3898 . . . . . . . . . . . . . . . 16 ({𝑦} ⊆ ran 𝐹 ↔ ({𝑦} ∩ ran 𝐹) = {𝑦})
155153, 154sylib 221 . . . . . . . . . . . . . . 15 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → ({𝑦} ∩ ran 𝐹) = {𝑦})
156151, 155eqtrd 2833 . . . . . . . . . . . . . 14 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = {𝑦})
157156iuneq2dv 4905 . . . . . . . . . . . . 13 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = ∪ 𝑦 ∈ 𝐵 {𝑦})
158 iunid 4947 . . . . . . . . . . . . 13 ∪ 𝑦 ∈ 𝐵 {𝑦} = 𝐵
159157, 158eqtrdi 2849 . . . . . . . . . . . 12 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = 𝐵)
160148, 159sseqtrd 3955 . . . . . . . . . . 11 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵)
161160ad2antrr 725 . . . . . . . . . 10 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵)
162144, 161eqsstrid 3963 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ⊆ 𝐵)
163143, 162sstrd 3925 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) ⊆ 𝐵)
16442adantr 484 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
165164ffund 6491 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → Fun 𝑓)
166 simpr 488 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵)
16755, 57syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ◡𝐹 ∈ V)
168167ad3antrrr 729 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ◡𝐹 ∈ V)
169 imaexg 7602 . . . . . . . . . . . . . . . 16 (◡𝐹 ∈ V → (◡𝐹 “ {𝑡}) ∈ V)
170168, 169syl 17 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ V)
1711, 131elrnmpt1s 5793 . . . . . . . . . . . . . . 15 ((𝑡 ∈ 𝐵 ∧ (◡𝐹 “ {𝑡}) ∈ V) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
172166, 170, 171syl2anc 587 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
173164fdmd 6497 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → dom 𝑓 = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))
174172, 173eleqtrrd 2893 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ dom 𝑓)
175 fvelrn 6821 . . . . . . . . . . . . 13 ((Fun 𝑓 ∧ (◡𝐹 “ {𝑡}) ∈ dom 𝑓) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓)
176165, 174, 175syl2anc 587 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓)
17715ad3antrrr 729 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝐹 Fn 𝐴)
178 simplr 768 . . . . . . . . . . . . . 14 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)
179 fveq2 6645 . . . . . . . . . . . . . . . . 17 (𝑧 = (◡𝐹 “ {𝑡}) → (𝑓‘𝑧) = (𝑓‘(◡𝐹 “ {𝑡})))
180 id 22 . . . . . . . . . . . . . . . . 17 (𝑧 = (◡𝐹 “ {𝑡}) → 𝑧 = (◡𝐹 “ {𝑡}))
181179, 180eleq12d 2884 . . . . . . . . . . . . . . . 16 (𝑧 = (◡𝐹 “ {𝑡}) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})))
182181rspcv 3566 . . . . . . . . . . . . . . 15 ((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})))
183182imp 410 . . . . . . . . . . . . . 14 (((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))
184172, 178, 183syl2anc 587 . . . . . . . . . . . . 13 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))
185 fniniseg 6807 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → ((𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}) ↔ ((𝑓‘(◡𝐹 “ {𝑡})) ∈ 𝐴 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)))
186185simplbda 503 . . . . . . . . . . . . 13 ((𝐹 Fn 𝐴 ∧ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)
187177, 184, 186syl2anc 587 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)
188 fveqeq2 6654 . . . . . . . . . . . . 13 (𝑘 = (𝑓‘(◡𝐹 “ {𝑡})) → ((𝐹‘𝑘) = 𝑡 ↔ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡))
189188rspcev 3571 . . . . . . . . . . . 12 (((𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡)
190176, 187, 189syl2anc 587 . . . . . . . . . . 11 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡)
19172adantr 484 . . . . . . . . . . . 12 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ran 𝑓 ⊆ 𝐴)
192177, 191fvelimabd 6713 . . . . . . . . . . 11 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑡 ∈ (𝐹 “ ran 𝑓) ↔ ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡))
193190, 192mpbird 260 . . . . . . . . . 10 (((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝐹 “ ran 𝑓))
194193ex 416 . . . . . . . . 9 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑡 ∈ 𝐵 → 𝑡 ∈ (𝐹 “ ran 𝑓)))
195194ssrdv 3921 . . . . . . . 8 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ⊆ (𝐹 “ ran 𝑓))
196163, 195eqssd 3932 . . . . . . 7 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) = 𝐵)
197140, 196jca 515 . . . . . 6 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵))
198 breq1 5033 . . . . . . . 8 (𝑥 = ran 𝑓 → (𝑥 ≈ 𝐵 ↔ ran 𝑓 ≈ 𝐵))
199 imaeq2 5892 . . . . . . . . 9 (𝑥 = ran 𝑓 → (𝐹 “ 𝑥) = (𝐹 “ ran 𝑓))
200199eqeq1d 2800 . . . . . . . 8 (𝑥 = ran 𝑓 → ((𝐹 “ 𝑥) = 𝐵 ↔ (𝐹 “ ran 𝑓) = 𝐵))
201198, 200anbi12d 633 . . . . . . 7 (𝑥 = ran 𝑓 → ((𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵) ↔ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)))
202201rspcev 3571 . . . . . 6 ((ran 𝑓 ∈ 𝒫 𝐴 ∧ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
20373, 197, 202syl2anc 587 . . . . 5 ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
204203anasss 470 . . . 4 (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
205204ex 416 . . 3 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)))
206205exlimdv 1934 . 2 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)))
20738, 206mpd 15 1 ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  ∪ cuni 4800  ∪ ciun 4881  Disj wdisj 4995   class class class wbr 5030   ↦ cmpt 5110   I cid 5424  ◡ccnv 5518  dom cdm 5519  ran crn 5520   “ cima 5522  Fun wfun 6318   Fn wfn 6319  ⟶wf 6320  –1-1→wf1 6321  –1-1-onto→wf1o 6323  ‘cfv 6324   ≈ cen 8489
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-ac2 9874
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-disj 4996  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-wrecs 7930  df-recs 7991  df-er 8272  df-en 8493  df-card 9352  df-ac 9527
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator