Step | Hyp | Ref
| Expression |
1 | | nfsbc1v 3754 |
. . 3
⊢
Ⅎ𝑦[(𝑓‘𝑥) / 𝑦]𝜑 |
2 | | sbceq1a 3745 |
. . 3
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
3 | 1, 2 | ac6gf 36046 |
. 2
⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) |
4 | | fdm 6669 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴) |
5 | | vex 3447 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
6 | 5 | dmex 7835 |
. . . . . . 7
⊢ dom 𝑓 ∈ V |
7 | 4, 6 | eqeltrrdi 2847 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → 𝐴 ∈ V) |
8 | | ffn 6660 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
9 | | fnrndomg 10402 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝑓 Fn 𝐴 → ran 𝑓 ≼ 𝐴)) |
10 | 7, 8, 9 | sylc 65 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ≼ 𝐴) |
11 | 10 | adantr 482 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ≼ 𝐴) |
12 | | frn 6667 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ⊆ 𝐵) |
13 | 12 | adantr 482 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ⊆ 𝐵) |
14 | | nfv 1917 |
. . . . . 6
⊢
Ⅎ𝑥 𝑓:𝐴⟶𝐵 |
15 | | nfra1 3265 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 |
16 | 14, 15 | nfan 1902 |
. . . . 5
⊢
Ⅎ𝑥(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) |
17 | | ffun 6663 |
. . . . . . . . . 10
⊢ (𝑓:𝐴⟶𝐵 → Fun 𝑓) |
18 | 17 | adantr 482 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → Fun 𝑓) |
19 | 4 | eleq2d 2823 |
. . . . . . . . . 10
⊢ (𝑓:𝐴⟶𝐵 → (𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ 𝐴)) |
20 | 19 | biimpar 479 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝑓) |
21 | | fvelrn 7019 |
. . . . . . . . 9
⊢ ((Fun
𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓) |
22 | 18, 20, 21 | syl2anc 585 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
23 | 22 | adantlr 713 |
. . . . . . 7
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
24 | | rspa 3229 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑) |
25 | 24 | adantll 712 |
. . . . . . 7
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑) |
26 | | rspesbca 3832 |
. . . . . . 7
⊢ (((𝑓‘𝑥) ∈ ran 𝑓 ∧ [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑦 ∈ ran 𝑓𝜑) |
27 | 23, 25, 26 | syl2anc 585 |
. . . . . 6
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ran 𝑓𝜑) |
28 | 27 | ex 414 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ ran 𝑓𝜑)) |
29 | 16, 28 | ralrimi 3238 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑) |
30 | | nfv 1917 |
. . . . . 6
⊢
Ⅎ𝑦 𝑓:𝐴⟶𝐵 |
31 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
32 | 31, 1 | nfralw 3292 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 |
33 | 30, 32 | nfan 1902 |
. . . . 5
⊢
Ⅎ𝑦(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) |
34 | | fvelrnb 6895 |
. . . . . . . 8
⊢ (𝑓 Fn 𝐴 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
35 | 8, 34 | syl 17 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
36 | 35 | adantr 482 |
. . . . . 6
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
37 | | rsp 3228 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑)) |
38 | 37 | adantl 483 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑)) |
39 | 2 | eqcoms 2745 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥) = 𝑦 → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
40 | 39 | biimprcd 250 |
. . . . . . . 8
⊢
([(𝑓‘𝑥) / 𝑦]𝜑 → ((𝑓‘𝑥) = 𝑦 → 𝜑)) |
41 | 38, 40 | syl6 35 |
. . . . . . 7
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ((𝑓‘𝑥) = 𝑦 → 𝜑))) |
42 | 16, 41 | reximdai 3242 |
. . . . . 6
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝜑)) |
43 | 36, 42 | sylbid 239 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 → ∃𝑥 ∈ 𝐴 𝜑)) |
44 | 33, 43 | ralrimi 3238 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑) |
45 | 5 | rnex 7836 |
. . . . 5
⊢ ran 𝑓 ∈ V |
46 | | breq1 5103 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (𝑐 ≼ 𝐴 ↔ ran 𝑓 ≼ 𝐴)) |
47 | | sseq1 3964 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (𝑐 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵)) |
48 | 46, 47 | anbi12d 632 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → ((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ↔ (ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵))) |
49 | | rexeq 3308 |
. . . . . . . 8
⊢ (𝑐 = ran 𝑓 → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ ran 𝑓𝜑)) |
50 | 49 | ralbidv 3172 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑)) |
51 | | raleq 3307 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) |
52 | 50, 51 | anbi12d 632 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → ((∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑))) |
53 | 48, 52 | anbi12d 632 |
. . . . 5
⊢ (𝑐 = ran 𝑓 → (((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) ↔ ((ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)))) |
54 | 45, 53 | spcev 3560 |
. . . 4
⊢ (((ran
𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
55 | 11, 13, 29, 44, 54 | syl22anc 837 |
. . 3
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
56 | 55 | exlimiv 1933 |
. 2
⊢
(∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
57 | 3, 56 | syl 17 |
1
⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |