Step | Hyp | Ref
| Expression |
1 | | eqid 2772 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) = (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
2 | 1 | elrnmpt 5665 |
. . . . . . . 8
⊢ (𝑧 ∈ V → (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦}))) |
3 | 2 | elv 3414 |
. . . . . . 7
⊢ (𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})) |
4 | | simpr 477 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 = (◡𝐹 “ {𝑦})) |
5 | | simpl3 1173 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐵 ⊆ ran 𝐹) |
6 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
7 | 5, 6 | sseldd 3853 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ran 𝐹) |
8 | | inisegn0 5795 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑦}) ≠ ∅) |
9 | 7, 8 | sylib 210 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ≠ ∅) |
10 | 9 | adantr 473 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → (◡𝐹 “ {𝑦}) ≠ ∅) |
11 | 4, 10 | eqnetrd 3028 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅) |
12 | 11 | r19.29an 3227 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ ∃𝑦 ∈ 𝐵 𝑧 = (◡𝐹 “ {𝑦})) → 𝑧 ≠ ∅) |
13 | 3, 12 | sylan2b 584 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝑧 ≠ ∅) |
14 | 13 | ralrimiva 3126 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ≠ ∅) |
15 | | simp2 1117 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 Fn 𝐴) |
16 | | simp1 1116 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐴 ∈ 𝑉) |
17 | 15, 16 | jca 504 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉)) |
18 | | fnex 6800 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
19 | | rnexg 7423 |
. . . . . . . . . 10
⊢ (𝐹 ∈ V → ran 𝐹 ∈ V) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ran 𝐹 ∈ V) |
21 | | simp3 1118 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ⊆ ran 𝐹) |
22 | 20, 21 | ssexd 5078 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐵 ∈ V) |
23 | | mptexg 6804 |
. . . . . . . 8
⊢ (𝐵 ∈ V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
24 | | rnexg 7423 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
25 | 22, 23, 24 | 3syl 18 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
26 | | fvi 6562 |
. . . . . . 7
⊢ (ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
28 | 27 | raleqdv 3349 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅ ↔ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ≠ ∅)) |
29 | 14, 28 | mpbird 249 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))𝑧 ≠ ∅) |
30 | | fvex 6506 |
. . . . 5
⊢ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∈ V |
31 | 30 | ac5b 9692 |
. . . 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 4716 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
34 | 27, 33 | feq23d 6333 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ↔ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
35 | 27 | raleqdv 3349 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧 ↔ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) |
36 | 34, 35 | anbi12d 621 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))) |
37 | 36 | exbidv 1880 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))⟶∪ ( I
‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ( I ‘ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))(𝑓‘𝑧) ∈ 𝑧) ↔ ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧))) |
38 | 32, 37 | mpbid 224 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) |
39 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
40 | 39 | rnex 7426 |
. . . . . . . 8
⊢ ran 𝑓 ∈ V |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ V) |
42 | | simplr 756 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
43 | | frn 6344 |
. . . . . . . . 9
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → ran 𝑓 ⊆ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
45 | | nfv 1873 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) |
46 | | nfcv 2926 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦𝑓 |
47 | | nfmpt1 5019 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
48 | 47 | nfrn 5661 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
49 | 48 | nfuni 4712 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑦∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
50 | 46, 48, 49 | nff 6334 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) |
51 | 45, 50 | nfan 1862 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
52 | | nfv 1873 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑦(𝑓‘𝑧) ∈ 𝑧 |
53 | 48, 52 | nfral 3168 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 |
54 | 51, 53 | nfan 1862 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦(((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) |
55 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → 𝐹 ∈ V) |
56 | 55 | ad3antrrr 717 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V) |
57 | | cnvexg 7438 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
58 | | imaexg 7429 |
. . . . . . . . . . . . . 14
⊢ (◡𝐹 ∈ V → (◡𝐹 “ {𝑦}) ∈ V) |
59 | 56, 57, 58 | 3syl 18 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V) |
60 | | cnvimass 5783 |
. . . . . . . . . . . . . . 15
⊢ (◡𝐹 “ {𝑦}) ⊆ dom 𝐹 |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ dom 𝐹) |
62 | | fndm 6282 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
63 | 15, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → dom 𝐹 = 𝐴) |
64 | 63 | ad3antrrr 717 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → dom 𝐹 = 𝐴) |
65 | 61, 64 | sseqtrd 3891 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ⊆ 𝐴) |
66 | 59, 65 | elpwd 4425 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴) |
67 | 66 | ex 405 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴)) |
68 | 54, 67 | ralrimi 3160 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴) |
69 | 1 | rnmptss 6703 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
𝐵 (◡𝐹 “ {𝑦}) ∈ 𝒫 𝐴 → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴) |
70 | 68, 69 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴) |
71 | | sspwuni 4882 |
. . . . . . . . 9
⊢ (ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝒫 𝐴 ↔ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴) |
72 | 70, 71 | sylib 210 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ⊆ 𝐴) |
73 | 44, 72 | sstrd 3862 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ⊆ 𝐴) |
74 | 41, 73 | elpwd 4425 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ∈ 𝒫 𝐴) |
75 | | fnfun 6280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
76 | 15, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → Fun 𝐹) |
77 | 76 | ad5antr 721 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Fun 𝐹) |
78 | | sndisj 4915 |
. . . . . . . . . . . . . . . . . . 19
⊢
Disj 𝑦 ∈
𝐵 {𝑦} |
79 | | disjpreima 30094 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐹 ∧ Disj 𝑦 ∈ 𝐵 {𝑦}) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦})) |
80 | 77, 78, 79 | sylancl 577 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦})) |
81 | | disjrnmpt 30095 |
. . . . . . . . . . . . . . . . . 18
⊢
(Disj 𝑦
∈ 𝐵 (◡𝐹 “ {𝑦}) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → Disj 𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧) |
83 | | simpllr 763 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
84 | | simplr 756 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
85 | | simp-4r 771 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) |
86 | | fveq2 6493 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑢 → (𝑓‘𝑧) = (𝑓‘𝑢)) |
87 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑢 → 𝑧 = 𝑢) |
88 | 86, 87 | eleq12d 2854 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 𝑢 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑢) ∈ 𝑢)) |
89 | 88 | rspcv 3525 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑢) ∈ 𝑢)) |
90 | 89 | imp 398 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑢) ∈ 𝑢) |
91 | 83, 85, 90 | syl2anc 576 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑢) |
92 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) = (𝑓‘𝑣)) |
93 | | fveq2 6493 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑣 → (𝑓‘𝑧) = (𝑓‘𝑣)) |
94 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑣 → 𝑧 = 𝑣) |
95 | 93, 94 | eleq12d 2854 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 𝑣 → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘𝑣) ∈ 𝑣)) |
96 | 95 | rspcv 3525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘𝑣) ∈ 𝑣)) |
97 | 96 | imp 398 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘𝑣) ∈ 𝑣) |
98 | 84, 85, 97 | syl2anc 576 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑣) ∈ 𝑣) |
99 | 92, 98 | eqeltrd 2860 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → (𝑓‘𝑢) ∈ 𝑣) |
100 | 87, 94 | disji 4908 |
. . . . . . . . . . . . . . . . 17
⊢
((Disj 𝑧
∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))𝑧 ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ((𝑓‘𝑢) ∈ 𝑢 ∧ (𝑓‘𝑢) ∈ 𝑣)) → 𝑢 = 𝑣) |
101 | 82, 83, 84, 91, 99, 100 | syl122anc 1359 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ (𝑓‘𝑢) = (𝑓‘𝑣)) → 𝑢 = 𝑣) |
102 | 101 | ex 405 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)) |
103 | 102 | anasss 459 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ (𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ 𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) → ((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)) |
104 | 103 | ralrimivva 3135 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣)) |
105 | 42, 104 | jca 504 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))) |
106 | | dff13 6832 |
. . . . . . . . . . . 12
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ↔ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑢 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))∀𝑣 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))((𝑓‘𝑢) = (𝑓‘𝑣) → 𝑢 = 𝑣))) |
107 | 105, 106 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
108 | | f1f1orn 6449 |
. . . . . . . . . . 11
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1→∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran
𝑓) |
109 | 107, 108 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran
𝑓) |
110 | | f1oen3g 8316 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ V ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))–1-1-onto→ran
𝑓) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓) |
111 | 39, 109, 110 | sylancr 578 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ ran 𝑓) |
112 | 111 | ensymd 8351 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
113 | 22, 23 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
114 | 113 | ad2antrr 713 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V) |
115 | 59 | ex 405 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → (◡𝐹 “ {𝑦}) ∈ V)) |
116 | 54, 115 | ralrimi 3160 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V) |
117 | 76 | ad5antr 721 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → Fun 𝐹) |
118 | | simpr 477 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ≠ 𝑡) |
119 | 21 | ad5antr 721 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝐵 ⊆ ran 𝐹) |
120 | | simpllr 763 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ 𝐵) |
121 | 119, 120 | sseldd 3853 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑦 ∈ ran 𝐹) |
122 | | simplr 756 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ 𝐵) |
123 | 119, 122 | sseldd 3853 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → 𝑡 ∈ ran 𝐹) |
124 | 117, 118,
121, 123 | preimane 30171 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) ∧ 𝑦 ≠ 𝑡) → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡})) |
125 | 124 | ex 405 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → (𝑦 ≠ 𝑡 → (◡𝐹 “ {𝑦}) ≠ (◡𝐹 “ {𝑡}))) |
126 | 125 | necon4d 2985 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) ∧ 𝑡 ∈ 𝐵) → ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)) |
127 | 126 | ralrimiva 3126 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑦 ∈ 𝐵) → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)) |
128 | 127 | ex 405 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 → ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))) |
129 | 54, 128 | ralrimi 3160 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡)) |
130 | 116, 129 | jca 504 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))) |
131 | | sneq 4445 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑡 → {𝑦} = {𝑡}) |
132 | 131 | imaeq2d 5764 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑡 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡})) |
133 | 1, 132 | f1mpt 6838 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V ↔ (∀𝑦 ∈ 𝐵 (◡𝐹 “ {𝑦}) ∈ V ∧ ∀𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐵 ((◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑡}) → 𝑦 = 𝑡))) |
134 | 130, 133 | sylibr 226 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V) |
135 | | f1f1orn 6449 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1→V → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
136 | 134, 135 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
137 | | f1oen3g 8316 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∈ V ∧ (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})):𝐵–1-1-onto→ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
138 | 114, 136,
137 | syl2anc 576 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
139 | 138 | ensymd 8351 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵) |
140 | | entr 8352 |
. . . . . . . 8
⊢ ((ran
𝑓 ≈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ≈ 𝐵) → ran 𝑓 ≈ 𝐵) |
141 | 112, 139,
140 | syl2anc 576 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ran 𝑓 ≈ 𝐵) |
142 | | imass2 5799 |
. . . . . . . . . . 11
⊢ (ran
𝑓 ⊆ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
143 | 43, 142 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
144 | 42, 143 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) ⊆ (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})))) |
145 | | imauni 6824 |
. . . . . . . . . 10
⊢ (𝐹 “ ∪ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) = ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) |
146 | | imaeq2 5760 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (◡𝐹 “ {𝑦}) → (𝐹 “ 𝑧) = (𝐹 “ (◡𝐹 “ {𝑦}))) |
147 | 55 | adantr 473 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ V) |
148 | 147, 57, 58 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (◡𝐹 “ {𝑦}) ∈ V) |
149 | 146, 148 | iunrnmptss 30080 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ ∪
𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦}))) |
150 | | funimacnv 6262 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝐹 → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹)) |
151 | 76, 150 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹)) |
152 | 151 | adantr 473 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = ({𝑦} ∩ ran 𝐹)) |
153 | 6 | snssd 4610 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ 𝐵) |
154 | 153, 5 | sstrd 3862 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → {𝑦} ⊆ ran 𝐹) |
155 | | df-ss 3837 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑦} ⊆ ran 𝐹 ↔ ({𝑦} ∩ ran 𝐹) = {𝑦}) |
156 | 154, 155 | sylib 210 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → ({𝑦} ∩ ran 𝐹) = {𝑦}) |
157 | 152, 156 | eqtrd 2808 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑦 ∈ 𝐵) → (𝐹 “ (◡𝐹 “ {𝑦})) = {𝑦}) |
158 | 157 | iuneq2dv 4809 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = ∪
𝑦 ∈ 𝐵 {𝑦}) |
159 | | iunid 4844 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑦 ∈ 𝐵 {𝑦} = 𝐵 |
160 | 158, 159 | syl6eq 2824 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑦 ∈ 𝐵 (𝐹 “ (◡𝐹 “ {𝑦})) = 𝐵) |
161 | 149, 160 | sseqtrd 3891 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵) |
162 | 161 | ad2antrr 713 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∪
𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝐹 “ 𝑧) ⊆ 𝐵) |
163 | 145, 162 | syl5eqss 3899 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ⊆ 𝐵) |
164 | 144, 163 | sstrd 3862 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) ⊆ 𝐵) |
165 | 42 | adantr 473 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
166 | 165 | ffund 6342 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → Fun 𝑓) |
167 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ 𝐵) |
168 | 55, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ◡𝐹 ∈ V) |
169 | 168 | ad3antrrr 717 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ◡𝐹 ∈ V) |
170 | | imaexg 7429 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝐹 ∈ V → (◡𝐹 “ {𝑡}) ∈ V) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ V) |
172 | 1, 132 | elrnmpt1s 5666 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝐵 ∧ (◡𝐹 “ {𝑡}) ∈ V) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
173 | 167, 171,
172 | syl2anc 576 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
174 | 165 | fdmd 6347 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → dom 𝑓 = ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) |
175 | 173, 174 | eleqtrrd 2863 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (◡𝐹 “ {𝑡}) ∈ dom 𝑓) |
176 | | fvelrn 6663 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑓 ∧ (◡𝐹 “ {𝑡}) ∈ dom 𝑓) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓) |
177 | 166, 175,
176 | syl2anc 576 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓) |
178 | 15 | ad3antrrr 717 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝐹 Fn 𝐴) |
179 | | simplr 756 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) |
180 | | fveq2 6493 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (◡𝐹 “ {𝑡}) → (𝑓‘𝑧) = (𝑓‘(◡𝐹 “ {𝑡}))) |
181 | | id 22 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (◡𝐹 “ {𝑡}) → 𝑧 = (◡𝐹 “ {𝑡})) |
182 | 180, 181 | eleq12d 2854 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (◡𝐹 “ {𝑡}) → ((𝑓‘𝑧) ∈ 𝑧 ↔ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))) |
183 | 182 | rspcv 3525 |
. . . . . . . . . . . . . . 15
⊢ ((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) → (∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧 → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}))) |
184 | 183 | imp 398 |
. . . . . . . . . . . . . 14
⊢ (((◡𝐹 “ {𝑡}) ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) |
185 | 173, 179,
184 | syl2anc 576 |
. . . . . . . . . . . . 13
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) |
186 | | fniniseg 6649 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn 𝐴 → ((𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡}) ↔ ((𝑓‘(◡𝐹 “ {𝑡})) ∈ 𝐴 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡))) |
187 | 186 | simplbda 492 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn 𝐴 ∧ (𝑓‘(◡𝐹 “ {𝑡})) ∈ (◡𝐹 “ {𝑡})) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) |
188 | 178, 185,
187 | syl2anc 576 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) |
189 | | fveqeq2 6502 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑓‘(◡𝐹 “ {𝑡})) → ((𝐹‘𝑘) = 𝑡 ↔ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡)) |
190 | 189 | rspcev 3529 |
. . . . . . . . . . . 12
⊢ (((𝑓‘(◡𝐹 “ {𝑡})) ∈ ran 𝑓 ∧ (𝐹‘(𝑓‘(◡𝐹 “ {𝑡}))) = 𝑡) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡) |
191 | 177, 188,
190 | syl2anc 576 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡) |
192 | 73 | adantr 473 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → ran 𝑓 ⊆ 𝐴) |
193 | 178, 192 | fvelimabd 6561 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → (𝑡 ∈ (𝐹 “ ran 𝑓) ↔ ∃𝑘 ∈ ran 𝑓(𝐹‘𝑘) = 𝑡)) |
194 | 191, 193 | mpbird 249 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) ∧ 𝑡 ∈ 𝐵) → 𝑡 ∈ (𝐹 “ ran 𝑓)) |
195 | 194 | ex 405 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝑡 ∈ 𝐵 → 𝑡 ∈ (𝐹 “ ran 𝑓))) |
196 | 195 | ssrdv 3858 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → 𝐵 ⊆ (𝐹 “ ran 𝑓)) |
197 | 164, 196 | eqssd 3869 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (𝐹 “ ran 𝑓) = 𝐵) |
198 | 141, 197 | jca 504 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)) |
199 | | breq1 4926 |
. . . . . . . 8
⊢ (𝑥 = ran 𝑓 → (𝑥 ≈ 𝐵 ↔ ran 𝑓 ≈ 𝐵)) |
200 | | imaeq2 5760 |
. . . . . . . . 9
⊢ (𝑥 = ran 𝑓 → (𝐹 “ 𝑥) = (𝐹 “ ran 𝑓)) |
201 | 200 | eqeq1d 2774 |
. . . . . . . 8
⊢ (𝑥 = ran 𝑓 → ((𝐹 “ 𝑥) = 𝐵 ↔ (𝐹 “ ran 𝑓) = 𝐵)) |
202 | 199, 201 | anbi12d 621 |
. . . . . . 7
⊢ (𝑥 = ran 𝑓 → ((𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵) ↔ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵))) |
203 | 202 | rspcev 3529 |
. . . . . 6
⊢ ((ran
𝑓 ∈ 𝒫 𝐴 ∧ (ran 𝑓 ≈ 𝐵 ∧ (𝐹 “ ran 𝑓) = 𝐵)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |
204 | 74, 198, 203 | syl2anc 576 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ 𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |
205 | 204 | anasss 459 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) ∧ (𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧)) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |
206 | 205 | ex 405 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ((𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))) |
207 | 206 | exlimdv 1892 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → (∃𝑓(𝑓:ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))⟶∪ ran
(𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦})) ∧ ∀𝑧 ∈ ran (𝑦 ∈ 𝐵 ↦ (◡𝐹 “ {𝑦}))(𝑓‘𝑧) ∈ 𝑧) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵))) |
208 | 38, 207 | mpd 15 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴 ∧ 𝐵 ⊆ ran 𝐹) → ∃𝑥 ∈ 𝒫 𝐴(𝑥 ≈ 𝐵 ∧ (𝐹 “ 𝑥) = 𝐵)) |