| Step | Hyp | Ref
| Expression |
| 1 | | nfsbc1v 3808 |
. . 3
⊢
Ⅎ𝑦[(𝑓‘𝑥) / 𝑦]𝜑 |
| 2 | | sbceq1a 3799 |
. . 3
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 3 | 1, 2 | ac6gf 37739 |
. 2
⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 4 | | fdm 6745 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴) |
| 5 | | vex 3484 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
| 6 | 5 | dmex 7931 |
. . . . . . 7
⊢ dom 𝑓 ∈ V |
| 7 | 4, 6 | eqeltrrdi 2850 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → 𝐴 ∈ V) |
| 8 | | ffn 6736 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
| 9 | | fnrndomg 10576 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝑓 Fn 𝐴 → ran 𝑓 ≼ 𝐴)) |
| 10 | 7, 8, 9 | sylc 65 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ≼ 𝐴) |
| 11 | 10 | adantr 480 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ≼ 𝐴) |
| 12 | | frn 6743 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ⊆ 𝐵) |
| 13 | 12 | adantr 480 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ⊆ 𝐵) |
| 14 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑥 𝑓:𝐴⟶𝐵 |
| 15 | | nfra1 3284 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 |
| 16 | 14, 15 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑥(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) |
| 17 | | ffun 6739 |
. . . . . . . . . 10
⊢ (𝑓:𝐴⟶𝐵 → Fun 𝑓) |
| 18 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → Fun 𝑓) |
| 19 | 4 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑓:𝐴⟶𝐵 → (𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ 𝐴)) |
| 20 | 19 | biimpar 477 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝑓) |
| 21 | | fvelrn 7096 |
. . . . . . . . 9
⊢ ((Fun
𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓) |
| 22 | 18, 20, 21 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
| 23 | 22 | adantlr 715 |
. . . . . . 7
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
| 24 | | rspa 3248 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑) |
| 25 | 24 | adantll 714 |
. . . . . . 7
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑) |
| 26 | | rspesbca 3881 |
. . . . . . 7
⊢ (((𝑓‘𝑥) ∈ ran 𝑓 ∧ [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑦 ∈ ran 𝑓𝜑) |
| 27 | 23, 25, 26 | syl2anc 584 |
. . . . . 6
⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ran 𝑓𝜑) |
| 28 | 27 | ex 412 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ ran 𝑓𝜑)) |
| 29 | 16, 28 | ralrimi 3257 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑) |
| 30 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑦 𝑓:𝐴⟶𝐵 |
| 31 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
| 32 | 31, 1 | nfralw 3311 |
. . . . . 6
⊢
Ⅎ𝑦∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 |
| 33 | 30, 32 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑦(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) |
| 34 | | fvelrnb 6969 |
. . . . . . . 8
⊢ (𝑓 Fn 𝐴 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
| 35 | 8, 34 | syl 17 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
| 36 | 35 | adantr 480 |
. . . . . 6
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦)) |
| 37 | | rsp 3247 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 38 | 37 | adantl 481 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 39 | 2 | eqcoms 2745 |
. . . . . . . . 9
⊢ ((𝑓‘𝑥) = 𝑦 → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 40 | 39 | biimprcd 250 |
. . . . . . . 8
⊢
([(𝑓‘𝑥) / 𝑦]𝜑 → ((𝑓‘𝑥) = 𝑦 → 𝜑)) |
| 41 | 38, 40 | syl6 35 |
. . . . . . 7
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ((𝑓‘𝑥) = 𝑦 → 𝜑))) |
| 42 | 16, 41 | reximdai 3261 |
. . . . . 6
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝜑)) |
| 43 | 36, 42 | sylbid 240 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 → ∃𝑥 ∈ 𝐴 𝜑)) |
| 44 | 33, 43 | ralrimi 3257 |
. . . 4
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑) |
| 45 | 5 | rnex 7932 |
. . . . 5
⊢ ran 𝑓 ∈ V |
| 46 | | breq1 5146 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (𝑐 ≼ 𝐴 ↔ ran 𝑓 ≼ 𝐴)) |
| 47 | | sseq1 4009 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (𝑐 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵)) |
| 48 | 46, 47 | anbi12d 632 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → ((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ↔ (ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵))) |
| 49 | | rexeq 3322 |
. . . . . . . 8
⊢ (𝑐 = ran 𝑓 → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ ran 𝑓𝜑)) |
| 50 | 49 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑)) |
| 51 | | raleq 3323 |
. . . . . . 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 3606 |
. . . 4
⊢ (((ran
𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
| 55 | 11, 13, 29, 44, 54 | syl22anc 839 |
. . 3
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
| 56 | 55 | exlimiv 1930 |
. 2
⊢
(∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |
| 57 | 3, 56 | syl 17 |
1
⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))) |