Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) = (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
2 | 1 | elrnmpt 5834 |
. . . . . . . 8
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦}))) |
3 | 2 | elv 3421 |
. . . . . . 7
⊢ (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})) |
4 | | simpr 488 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 = (◡𝐹 “ {𝑦})) |
5 | | simpl3 1195 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐵 ⊆ ran 𝐹) |
6 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
7 | 5, 6 | sseldd 3911 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ran 𝐹) |
8 | | inisegn0 5975 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑦}) ≠ ∅) |
9 | 7, 8 | sylib 221 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ≠ ∅) |
10 | 9 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → (◡𝐹 “ {𝑦}) ≠ ∅) |
11 | 4, 10 | eqnetrd 3009 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅) |
12 | 11 | r19.29an 3214 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅) |
13 | 3, 12 | sylan2b 597 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝑧 ≠ ∅) |
14 | 13 | ralrimiva 3106 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ≠ ∅) |
15 | | simp2 1139 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 Fn 𝐴) |
16 | | simp1 1138 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐴 ∈ 𝑉) |
17 | 15, 16 | jca 515 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉)) |
18 | | fnex 7042 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
19 | | rnexg 7691 |
. . . . . . . . . 10
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ran 𝐹 ∈ V) |
21 | | simp3 1140 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ⊆ ran 𝐹) |
22 | 20, 21 | ssexd 5226 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ∈ V) |
23 | | mptexg 7046 |
. . . . . . . 8
⊢ (𝐵 ∈ V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
24 | | rnexg 7691 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
26 | | fvi 6796 |
. . . . . . 7
⊢ (ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
28 | 27 | raleqdv 3332 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅ ↔ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ≠ ∅)) |
29 | 14, 28 | mpbird 260 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅) |
30 | | fvex 6739 |
. . . . 5
⊢ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∈ V |
31 | 30 | ac5b 10105 |
. . . 4
⊢
(∀𝑧 ∈ (
I ‘ran (𝑦 ∈
𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅ → ∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧)) |
32 | 29, 31 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧)) |
33 | 27 | unieqd 4842 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
34 | 27, 33 | feq23d 6549 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ↔ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
35 | 27 | raleqdv 3332 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧 ↔ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) |
36 | 34, 35 | anbi12d 634 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))) |
37 | 36 | exbidv 1929 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))) |
38 | 32, 37 | mpbid 235 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) |
39 | | vex 3419 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
40 | 39 | rnex 7699 |
. . . . . . . 8
⊢ ran 𝑓 ∈ V |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ V) |
42 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
43 | | frn 6561 |
. . . . . . . . 9
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → ran 𝑓 ⊆ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
45 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) |
46 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦𝑓 |
47 | | nfmpt1 5162 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
48 | 47 | nfrn 5830 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
49 | 48 | nfuni 4835 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
50 | 46, 48, 49 | nff 6550 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
51 | 45, 50 | nfan 1907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
52 | | nfv 1922 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝑓‘𝑧) ∈ 𝑧 |
53 | 48, 52 | nfralw 3148 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 |
54 | 51, 53 | nfan 1907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) |
55 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 ∈ V) |
56 | 55 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V) |
57 | | cnvexg 7711 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
58 | | imaexg 7702 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹 ∈ V → (◡𝐹 “ {𝑦}) ∈ V) |
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V) |
60 | | cnvimass 5958 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ {𝑦}) ⊆ dom 𝐹 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ dom 𝐹) |
62 | 15 | fndmd 6492 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → dom 𝐹 = 𝐴) |
63 | 62 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → dom 𝐹 = 𝐴) |
64 | 61, 63 | sseqtrd 3950 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ 𝐴) |
65 | 59, 64 | elpwd 4530 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴) |
66 | 65 | ex 416 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴)) |
67 | 54, 66 | ralrimi 3138 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴) |
68 | 1 | rnmptss 6948 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴 → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴) |
69 | 67, 68 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴) |
70 | | sspwuni 5017 |
. . . . . . . . 9
⊢ (ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴 ↔ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴) |
71 | 69, 70 | sylib 221 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴) |
72 | 44, 71 | sstrd 3920 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ 𝐴) |
73 | 41, 72 | elpwd 4530 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ 𝒫 𝐴) |
74 | | fnfun 6488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
75 | 15, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → Fun 𝐹) |
76 | 75 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Fun 𝐹) |
77 | | sndisj 5053 |
. . . . . . . . . . . . . . . . . . 19
⊢
Disj 𝑦 ∈
𝐵 {𝑦} |
78 | | disjpreima 30655 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐹 ∧ Disj 𝑦 ∈ 𝐵 {𝑦}) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦})) |
79 | 76, 77, 78 | sylancl 589 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦})) |
80 | | disjrnmpt 30656 |
. . . . . . . . . . . . . . . . . 18
⊢
(Disj 𝑦
∈ 𝐵 (◡𝐹 “ {𝑦}) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧) |
82 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
83 | | simplr 769 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
84 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) |
85 | | fveq2 6726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢)) |
86 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑢 → 𝑧 = 𝑢) |
87 | 85, 86 | eleq12d 2833 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢)) |
88 | 87 | rspcv 3539 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑢) ∈ 𝑢)) |
89 | 88 | imp 410 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑢) ∈ 𝑢) |
90 | 82, 84, 89 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑢) |
91 | | simpr 488 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) = (𝑓‘𝑣)) |
92 | | fveq2 6726 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑣 → (𝑓‘𝑧) = (𝑓‘𝑣)) |
93 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑣 → 𝑧 = 𝑣) |
94 | 92, 93 | eleq12d 2833 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑣 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑣) ∈ 𝑣)) |
95 | 94 | rspcv 3539 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑣) ∈ 𝑣)) |
96 | 95 | imp 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑣) ∈ 𝑣) |
97 | 83, 84, 96 | syl2anc 587 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑣) ∈ 𝑣) |
98 | 91, 97 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑣) |
99 | 86, 93 | disji 5045 |
. . . . . . . . . . . . . . . . 17
⊢
((Disj 𝑧
∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ((𝑓‘𝑢) ∈ 𝑢 ∧ (𝑓‘𝑢) ∈ 𝑣)) → 𝑢 = 𝑣) |
100 | 81, 82, 83, 90, 98, 99 | syl122anc 1381 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 = 𝑣) |
101 | 100 | ex 416 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)) |
102 | 101 | anasss 470 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)) |
103 | 102 | ralrimivva 3113 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)) |
104 | 42, 103 | jca 515 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))) |
105 | | dff13 7076 |
. . . . . . . . . . . 12
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))) |
106 | 104, 105 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
107 | | f1f1orn 6681 |
. . . . . . . . . . 11
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran
𝑓) |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran
𝑓) |
109 | | f1oen3g 8653 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ V ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran
𝑓) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓) |
110 | 39, 108, 109 | sylancr 590 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓) |
111 | 110 | ensymd 8690 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
112 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
113 | 112 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
114 | 59 | ex 416 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ V)) |
115 | 54, 114 | ralrimi 3138 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V) |
116 | 75 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → Fun 𝐹) |
117 | | simpr 488 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ≠ 𝑡) |
118 | 21 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝐵 ⊆ ran 𝐹) |
119 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ 𝐵) |
120 | 118, 119 | sseldd 3911 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ ran 𝐹) |
121 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ 𝐵) |
122 | 118, 121 | sseldd 3911 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ ran 𝐹) |
123 | 116, 117,
120, 122 | preimane 30740 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡})) |
124 | 123 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (𝑦 ≠ 𝑡 → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡}))) |
125 | 124 | necon4d 2965 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)) |
126 | 125 | ralrimiva 3106 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)) |
127 | 126 | ex 416 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))) |
128 | 54, 127 | ralrimi 3138 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)) |
129 | 115, 128 | jca 515 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))) |
130 | | sneq 4560 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑡 → {𝑦} = {𝑡}) |
131 | 130 | imaeq2d 5938 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑡 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡})) |
132 | 1, 131 | f1mpt 7082 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V ↔ (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))) |
133 | 129, 132 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V) |
134 | | f1f1orn 6681 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
135 | 133, 134 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
136 | | f1oen3g 8653 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V ∧ (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
137 | 113, 135,
136 | syl2anc 587 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
138 | 137 | ensymd 8690 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵) |
139 | | entr 8691 |
. . . . . . . 8
⊢ ((ran
𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵) → ran 𝑓 ≈ 𝐵) |
140 | 111, 138,
139 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ 𝐵) |
141 | | imass2 5979 |
. . . . . . . . . . 11
⊢ (ran
𝑓 ⊆ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
142 | 43, 141 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
143 | 42, 142 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
144 | | imauni 7068 |
. . . . . . . . . 10
⊢ (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) |
145 | | imaeq2 5934 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (◡𝐹 “ {𝑦}) → (𝐹 “ 𝑧) = (𝐹 “ (◡𝐹 “ {𝑦}))) |
146 | 55 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V) |
147 | 146, 57, 58 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V) |
148 | 145, 147 | iunrnmptss 30637 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ ∪
𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦}))) |
149 | | funimacnv 6470 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝐹 → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹)) |
150 | 75, 149 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹)) |
151 | 150 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹)) |
152 | 6 | snssd 4731 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ 𝐵) |
153 | 152, 5 | sstrd 3920 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ ran 𝐹) |
154 | | df-ss 3892 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑦} ⊆ ran 𝐹 ↔ ({𝑦} ∩ ran 𝐹) = {𝑦}) |
155 | 153, 154 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → ({𝑦} ∩ ran 𝐹) = {𝑦}) |
156 | 151, 155 | eqtrd 2778 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = {𝑦}) |
157 | 156 | iuneq2dv 4937 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = ∪
𝑦 ∈ 𝐵 {𝑦}) |
158 | | iunid 4978 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑦 ∈ 𝐵 {𝑦} = 𝐵 |
159 | 157, 158 | eqtrdi 2795 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = 𝐵) |
160 | 148, 159 | sseqtrd 3950 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵) |
161 | 160 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵) |
162 | 144, 161 | eqsstrid 3958 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ⊆ 𝐵) |
163 | 143, 162 | sstrd 3920 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) ⊆ 𝐵) |
164 | 42 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
165 | 164 | ffund 6558 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → Fun 𝑓) |
166 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵) |
167 | 55, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ◡𝐹 ∈ V) |
168 | 167 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ◡𝐹 ∈ V) |
169 | | imaexg 7702 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝐹 ∈ V → (◡𝐹 “ {𝑡}) ∈ V) |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ V) |
171 | 1, 131 | elrnmpt1s 5835 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝐵 ∧ (◡𝐹 “ {𝑡}) ∈ V) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
172 | 166, 170,
171 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
173 | 164 | fdmd 6565 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → dom 𝑓 = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
174 | 172, 173 | eleqtrrd 2842 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ dom 𝑓) |
175 | | fvelrn 6906 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (◡𝐹 “ {𝑡}) ∈ dom 𝑓) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓) |
176 | 165, 174,
175 | syl2anc 587 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓) |
177 | 15 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝐹 Fn 𝐴) |
178 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) |
179 | | fveq2 6726 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (◡𝐹 “ {𝑡}) → (𝑓‘𝑧) = (𝑓‘(◡𝐹 “ {𝑡}))) |
180 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (◡𝐹 “ {𝑡}) → 𝑧 = (◡𝐹 “ {𝑡})) |
181 | 179, 180 | eleq12d 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (◡𝐹 “ {𝑡}) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))) |
182 | 181 | rspcv 3539 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))) |
183 | 182 | imp 410 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) |
184 | 172, 178,
183 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) |
185 | | fniniseg 6889 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → ((𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}) ↔ ((𝑓‘(◡𝐹 “ {𝑡})) ∈ 𝐴 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡))) |
186 | 185 | simplbda 503 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝐴 ∧ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) |
187 | 177, 184,
186 | syl2anc 587 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) |
188 | | fveqeq2 6735 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑓‘(◡𝐹 “ {𝑡})) → ((𝐹‘𝑘) = 𝑡 ↔ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)) |
189 | 188 | rspcev 3544 |
. . . . . . . . . . . 12
⊢ (((𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡) |
190 | 176, 187,
189 | syl2anc 587 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡) |
191 | 72 | adantr 484 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ran 𝑓 ⊆ 𝐴) |
192 | 177, 191 | fvelimabd 6794 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑡 ∈ (𝐹 “ ran 𝑓) ↔ ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡)) |
193 | 190, 192 | mpbird 260 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝐹 “ ran 𝑓)) |
194 | 193 | ex 416 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑡 ∈ 𝐵 → 𝑡 ∈ (𝐹 “ ran 𝑓))) |
195 | 194 | ssrdv 3916 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ⊆ (𝐹 “ ran 𝑓)) |
196 | 163, 195 | eqssd 3927 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) = 𝐵) |
197 | 140, 196 | jca 515 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)) |
198 | | breq1 5065 |
. . . . . . . 8
⊢ (𝑥 = ran 𝑓 → (𝑥 ≈ 𝐵 ↔ ran 𝑓 ≈ 𝐵)) |
199 | | imaeq2 5934 |
. . . . . . . . 9
⊢ (𝑥 = ran 𝑓 → (𝐹 “ 𝑥) = (𝐹 “ ran 𝑓)) |
200 | 199 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑥 = ran 𝑓 → ((𝐹 “ 𝑥) = 𝐵 ↔ (𝐹 “ ran 𝑓) = 𝐵)) |
201 | 198, 200 | anbi12d 634 |
. . . . . . 7
⊢ (𝑥 = ran 𝑓 → ((𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵) ↔ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵))) |
202 | 201 | rspcev 3544 |
. . . . . 6
⊢ ((ran
𝑓 ∈ 𝒫 𝐴 ∧ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |
203 | 73, 197, 202 | syl2anc 587 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |
204 | 203 | anasss 470 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |
205 | 204 | ex 416 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))) |
206 | 205 | exlimdv 1941 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))) |
207 | 38, 206 | mpd 15 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |