Step | Hyp | Ref
| Expression |
1 | | nfsbc1v 3422 |
. . 3
⊢
Ⅎ𝑦[(𝑓‘𝑥) / 𝑦]𝜑 |
2 | | sbceq1a 3413 |
. . 3
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
3 | 1, 2 | ac6gf 32697 |
. 2
⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) |
4 | | fdm 5964 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴) |
5 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
6 | 5 | dmex 6991 |
. . . . . . 7
⊢ dom 𝑓 ∈ V |
7 | 4, 6 | syl6eqelr 2697 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → 𝐴 ∈ V) |
8 | | ffn 5958 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
9 | | fnrndomg 9239 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝑓 Fn 𝐴 → ran 𝑓 ≼ 𝐴)) |
10 | 7, 8, 9 | sylc 63 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ≼ 𝐴) |
11 | 10 | adantr 480 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ≼ 𝐴) |
12 | | frn 5966 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ⊆ 𝐵) |
13 | 12 | adantr 480 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ⊆ 𝐵) |
14 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑥 𝑓:𝐴⟶𝐵 |
15 | | nfra1 2925 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 |
16 | 14, 15 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑥(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) |
17 | | ffun 5961 |
. . . . . . . . . 10
⊢ (𝑓:𝐴⟶𝐵 → Fun 𝑓) |
18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → Fun 𝑓) |
19 | 4 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝑓:𝐴⟶𝐵 → (𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ 𝐴)) |
20 | 19 | biimpar 501 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝑓) |
21 | | fvelrn 6260 |
. . . . . . . . 9
⊢ ((Fun
𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓) |
22 | 18, 20, 21 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
23 | 22 | adantlr 747 |
. . . . . . 7
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
24 | | rspa 2914 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑) |
25 | 24 | adantll 746 |
. . . . . . 7
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑) |
26 | | rspesbca 3486 |
. . . . . . 7
⊢ (((𝑓‘𝑥) ∈ ran 𝑓 ∧ [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑦 ∈ ran 𝑓𝜑) |
27 | 23, 25, 26 | syl2anc 691 |
. . . . . 6
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ran 𝑓𝜑) |
28 | 27 | ex 449 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ ran 𝑓𝜑)) |
29 | 16, 28 | ralrimi 2940 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑) |
30 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑦 𝑓:𝐴⟶𝐵 |
31 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
32 | 31, 1 | nfral 2929 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 |
33 | 30, 32 | nfan 1816 |
. . . . 5
⊢
Ⅎ𝑦(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) |
34 | | fvelrnb 6153 |
. . . . . . . 8
⊢ (𝑓 Fn 𝐴 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
35 | 8, 34 | syl 17 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
37 | | rsp 2913 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑)) |
38 | 37 | adantl 481 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑)) |
39 | 2 | eqcoms 2618 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥) = 𝑦 → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
40 | 39 | biimprcd 239 |
. . . . . . . 8
⊢
([(𝑓‘𝑥) / 𝑦]𝜑 → ((𝑓‘𝑥) = 𝑦 → 𝜑)) |
41 | 38, 40 | syl6 34 |
. . . . . . 7
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ((𝑓‘𝑥) = 𝑦 → 𝜑))) |
42 | 16, 41 | reximdai 2995 |
. . . . . 6
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝜑)) |
43 | 36, 42 | sylbid 229 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 → ∃𝑥 ∈ 𝐴 𝜑)) |
44 | 33, 43 | ralrimi 2940 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑) |
45 | 5 | rnex 6992 |
. . . . 5
⊢ ran 𝑓 ∈ V |
46 | | breq1 4586 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (𝑐 ≼ 𝐴 ↔ ran 𝑓 ≼ 𝐴)) |
47 | | sseq1 3589 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (𝑐 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵)) |
48 | 46, 47 | anbi12d 743 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → ((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ↔ (ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵))) |
49 | | rexeq 3116 |
. . . . . . . 8
⊢ (𝑐 = ran 𝑓 → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ ran 𝑓𝜑)) |
50 | 49 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑)) |
51 | | raleq 3115 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) |
52 | 50, 51 | anbi12d 743 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → ((∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑))) |
53 | 48, 52 | anbi12d 743 |
. . . . 5
⊢ (𝑐 = ran 𝑓 → (((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) ↔ ((ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)))) |
54 | 45, 53 | spcev 3273 |
. . . 4
⊢ (((ran
𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
55 | 11, 13, 29, 44, 54 | syl22anc 1319 |
. . 3
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
56 | 55 | exlimiv 1845 |
. 2
⊢
(∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
57 | 3, 56 | syl 17 |
1
⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |