Step | Hyp | Ref
| Expression |
1 | | cfsetsnfsetfv.f |
. . 3
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} |
2 | | cfsetsnfsetfv.g |
. . 3
⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} |
3 | | cfsetsnfsetfv.h |
. . 3
⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) |
4 | 1, 2, 3 | cfsetsnfsetf 44239 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺⟶𝐹) |
5 | | vex 3419 |
. . . . 5
⊢ 𝑚 ∈ V |
6 | | feq1 6535 |
. . . . . 6
⊢ (𝑓 = 𝑚 → (𝑓:𝐴⟶𝐵 ↔ 𝑚:𝐴⟶𝐵)) |
7 | | fveq1 6725 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑚 → (𝑓‘𝑧) = (𝑚‘𝑧)) |
8 | 7 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑓 = 𝑚 ∧ 𝑧 ∈ 𝐴) → (𝑓‘𝑧) = (𝑚‘𝑧)) |
9 | 8 | eqeq1d 2740 |
. . . . . . . 8
⊢ ((𝑓 = 𝑚 ∧ 𝑧 ∈ 𝐴) → ((𝑓‘𝑧) = 𝑏 ↔ (𝑚‘𝑧) = 𝑏)) |
10 | 9 | ralbidva 3118 |
. . . . . . 7
⊢ (𝑓 = 𝑚 → (∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏 ↔ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏)) |
11 | 10 | rexbidv 3223 |
. . . . . 6
⊢ (𝑓 = 𝑚 → (∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏 ↔ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏)) |
12 | 6, 11 | anbi12d 634 |
. . . . 5
⊢ (𝑓 = 𝑚 → ((𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏) ↔ (𝑚:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏))) |
13 | 5, 12, 1 | elab2 3598 |
. . . 4
⊢ (𝑚 ∈ 𝐹 ↔ (𝑚:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏)) |
14 | | simpllr 776 |
. . . . . . . . . . 11
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) ∧ 𝑦 ∈ {𝑌}) → 𝑏 ∈ 𝐵) |
15 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑌} ↦ 𝑏) = (𝑦 ∈ {𝑌} ↦ 𝑏) |
16 | 14, 15 | fmptd 6940 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → (𝑦 ∈ {𝑌} ↦ 𝑏):{𝑌}⟶𝐵) |
17 | | snex 5333 |
. . . . . . . . . . . 12
⊢ {𝑌} ∈ V |
18 | 17 | mptex 7048 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑌} ↦ 𝑏) ∈ V |
19 | | feq1 6535 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 ∈ {𝑌} ↦ 𝑏) → (𝑥:{𝑌}⟶𝐵 ↔ (𝑦 ∈ {𝑌} ↦ 𝑏):{𝑌}⟶𝐵)) |
20 | 18, 19, 2 | elab2 3598 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ {𝑌} ↦ 𝑏) ∈ 𝐺 ↔ (𝑦 ∈ {𝑌} ↦ 𝑏):{𝑌}⟶𝐵) |
21 | 16, 20 | sylibr 237 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → (𝑦 ∈ {𝑌} ↦ 𝑏) ∈ 𝐺) |
22 | | fveq1 6725 |
. . . . . . . . . . . 12
⊢ (𝑛 = (𝑦 ∈ {𝑌} ↦ 𝑏) → (𝑛‘𝑌) = ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) |
23 | 22 | mpteq2dv 5160 |
. . . . . . . . . . 11
⊢ (𝑛 = (𝑦 ∈ {𝑌} ↦ 𝑏) → (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌)) = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))) |
24 | 23 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑦 ∈ {𝑌} ↦ 𝑏) → (𝑚 = (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌)) ↔ 𝑚 = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)))) |
25 | 24 | adantl 485 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) ∧ 𝑛 = (𝑦 ∈ {𝑌} ↦ 𝑏)) → (𝑚 = (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌)) ↔ 𝑚 = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)))) |
26 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) → (𝑚‘𝑧) = 𝑏) |
27 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) → (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))) |
28 | | eqidd 2739 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) ∧ 𝑎 = 𝑧) → (𝑦 ∈ {𝑌} ↦ 𝑏) = (𝑦 ∈ {𝑌} ↦ 𝑏)) |
29 | | eqidd 2739 |
. . . . . . . . . . . . . . . 16
⊢
((((((((𝐴 ∈
𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) ∧ 𝑎 = 𝑧) ∧ 𝑦 = 𝑌) → 𝑏 = 𝑏) |
30 | | snidg 4584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ {𝑌}) |
31 | 30 | ad6antlr 737 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) ∧ 𝑎 = 𝑧) → 𝑌 ∈ {𝑌}) |
32 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) → 𝑏 ∈ 𝐵) |
33 | 32 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) ∧ 𝑎 = 𝑧) → 𝑏 ∈ 𝐵) |
34 | 28, 29, 31, 33 | fvmptd 6834 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝐴 ∈
𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) ∧ 𝑎 = 𝑧) → ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌) = 𝑏) |
35 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
36 | 35 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) → 𝑧 ∈ 𝐴) |
37 | 27, 34, 36, 32 | fvmptd 6834 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) → ((𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))‘𝑧) = 𝑏) |
38 | 26, 37 | eqtr4d 2781 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) ∧ (𝑚‘𝑧) = 𝑏) → (𝑚‘𝑧) = ((𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))‘𝑧)) |
39 | 38 | ex 416 |
. . . . . . . . . . . 12
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ 𝑧 ∈ 𝐴) → ((𝑚‘𝑧) = 𝑏 → (𝑚‘𝑧) = ((𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))‘𝑧))) |
40 | 39 | ralimdva 3101 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏 → ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = ((𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))‘𝑧))) |
41 | 40 | imp 410 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = ((𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))‘𝑧)) |
42 | | ffn 6554 |
. . . . . . . . . . . . . . 15
⊢ (𝑚:𝐴⟶𝐵 → 𝑚 Fn 𝐴) |
43 | 42 | adantl 485 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) → 𝑚 Fn 𝐴) |
44 | | nfv 1922 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑎((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) |
45 | | fvexd 6741 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑎 ∈ 𝐴) → ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌) ∈ V) |
46 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) |
47 | 44, 45, 46 | fnmptd 6528 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) → (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) Fn 𝐴) |
48 | 43, 47 | jca 515 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) → (𝑚 Fn 𝐴 ∧ (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) Fn 𝐴)) |
49 | 48 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) → (𝑚 Fn 𝐴 ∧ (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) Fn 𝐴)) |
50 | 49 | adantr 484 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → (𝑚 Fn 𝐴 ∧ (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) Fn 𝐴)) |
51 | | eqfnfv 6861 |
. . . . . . . . . . 11
⊢ ((𝑚 Fn 𝐴 ∧ (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) Fn 𝐴) → (𝑚 = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) ↔ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = ((𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))‘𝑧))) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → (𝑚 = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌)) ↔ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = ((𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))‘𝑧))) |
53 | 41, 52 | mpbird 260 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → 𝑚 = (𝑎 ∈ 𝐴 ↦ ((𝑦 ∈ {𝑌} ↦ 𝑏)‘𝑌))) |
54 | 21, 25, 53 | rspcedvd 3547 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → ∃𝑛 ∈ 𝐺 𝑚 = (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌))) |
55 | | simp-4l 783 |
. . . . . . . . . . 11
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → 𝐴 ∈ 𝑉) |
56 | 1, 2, 3 | cfsetsnfsetfv 44238 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ 𝐺) → (𝐻‘𝑛) = (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌))) |
57 | 55, 56 | sylan 583 |
. . . . . . . . . 10
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) ∧ 𝑛 ∈ 𝐺) → (𝐻‘𝑛) = (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌))) |
58 | 57 | eqeq2d 2749 |
. . . . . . . . 9
⊢
((((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) ∧ 𝑛 ∈ 𝐺) → (𝑚 = (𝐻‘𝑛) ↔ 𝑚 = (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌)))) |
59 | 58 | rexbidva 3222 |
. . . . . . . 8
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → (∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛) ↔ ∃𝑛 ∈ 𝐺 𝑚 = (𝑎 ∈ 𝐴 ↦ (𝑛‘𝑌)))) |
60 | 54, 59 | mpbird 260 |
. . . . . . 7
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) ∧ ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → ∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛)) |
61 | 60 | ex 416 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) ∧ 𝑏 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏 → ∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛))) |
62 | 61 | rexlimdva 3210 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑚:𝐴⟶𝐵) → (∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏 → ∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛))) |
63 | 62 | expimpd 457 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((𝑚:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑚‘𝑧) = 𝑏) → ∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛))) |
64 | 13, 63 | syl5bi 245 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑚 ∈ 𝐹 → ∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛))) |
65 | 64 | ralrimiv 3105 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ∀𝑚 ∈ 𝐹 ∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛)) |
66 | | dffo3 6930 |
. 2
⊢ (𝐻:𝐺–onto→𝐹 ↔ (𝐻:𝐺⟶𝐹 ∧ ∀𝑚 ∈ 𝐹 ∃𝑛 ∈ 𝐺 𝑚 = (𝐻‘𝑛))) |
67 | 4, 65, 66 | sylanbrc 586 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺–onto→𝐹) |