Step | Hyp | Ref
| Expression |
1 | | choicefi.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | mptfi 9388 |
. . 3
⊢ (𝐴 ∈ Fin → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin) |
3 | | rnfi 9377 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin) |
4 | | fnchoice 44966 |
. . 3
⊢ (ran
(𝑥 ∈ 𝐴 ↦ 𝐵) ∈ Fin → ∃𝑔(𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦))) |
5 | 1, 2, 3, 4 | 4syl 19 |
. 2
⊢ (𝜑 → ∃𝑔(𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦))) |
6 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦))) → 𝜑) |
7 | | simprl 771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦))) → 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
8 | | nfv 1911 |
. . . . . . . 8
⊢
Ⅎ𝑦𝜑 |
9 | | nfra1 3281 |
. . . . . . . 8
⊢
Ⅎ𝑦∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) |
10 | 8, 9 | nfan 1896 |
. . . . . . 7
⊢
Ⅎ𝑦(𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) |
11 | | rspa 3245 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) |
12 | 11 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) |
13 | | vex 3481 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
14 | | eqid 2734 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
15 | 14 | elrnmpt 5971 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
16 | 13, 15 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝐵) |
17 | 16 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 = 𝐵) |
18 | 17 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → ∃𝑥 ∈ 𝐴 𝑦 = 𝐵) |
19 | | simp3 1137 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
20 | | choicefi.n |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≠ ∅) |
21 | 20 | 3adant3 1131 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) → 𝐵 ≠ ∅) |
22 | 19, 21 | eqnetrd 3005 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) → 𝑦 ≠ ∅) |
23 | 22 | 3exp 1118 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 = 𝐵 → 𝑦 ≠ ∅))) |
24 | 23 | rexlimdv 3150 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 → 𝑦 ≠ ∅)) |
25 | 24 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (∃𝑥 ∈ 𝐴 𝑦 = 𝐵 → 𝑦 ≠ ∅)) |
26 | 18, 25 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ≠ ∅) |
27 | 26 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑦 ≠ ∅) |
28 | | id 22 |
. . . . . . . . . . . 12
⊢ ((𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → (𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) |
29 | 28 | imp 406 |
. . . . . . . . . . 11
⊢ (((𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) ∧ 𝑦 ≠ ∅) → (𝑔‘𝑦) ∈ 𝑦) |
30 | 12, 27, 29 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) ∧ 𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑔‘𝑦) ∈ 𝑦) |
31 | 30 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑔‘𝑦) ∈ 𝑦)) |
32 | 10, 31 | ralrimi 3254 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) |
33 | | rsp 3244 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦 → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑔‘𝑦) ∈ 𝑦)) |
34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → (𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑔‘𝑦) ∈ 𝑦)) |
35 | 10, 34 | ralrimi 3254 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) |
36 | 35 | adantrl 716 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦))) → ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) |
37 | | vex 3481 |
. . . . . . . . 9
⊢ 𝑔 ∈ V |
38 | 37 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑔 ∈ V) |
39 | 1 | mptexd 7243 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) |
40 | | coexg 7951 |
. . . . . . . 8
⊢ ((𝑔 ∈ V ∧ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ V) |
41 | 38, 39, 40 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ V) |
42 | 41 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) → (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ V) |
43 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
44 | | choicefi.b |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
45 | 44 | ralrimiva 3143 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
46 | 14 | fnmpt 6708 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ 𝑊 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
47 | 45, 46 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
48 | 47 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
49 | | ssidd 4018 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
50 | | fnco 6686 |
. . . . . . . . 9
⊢ ((𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ∧ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ⊆ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) Fn 𝐴) |
51 | 43, 48, 49, 50 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) Fn 𝐴) |
52 | 51 | 3adant3 1131 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) → (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) Fn 𝐴) |
53 | | nfv 1911 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝜑 |
54 | | nfcv 2902 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑔 |
55 | | nfmpt1 5255 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
56 | 55 | nfrn 5965 |
. . . . . . . . . 10
⊢
Ⅎ𝑥ran
(𝑥 ∈ 𝐴 ↦ 𝐵) |
57 | 54, 56 | nffn 6667 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) |
58 | | nfv 1911 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑔‘𝑦) ∈ 𝑦 |
59 | 56, 58 | nfralw 3308 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦 |
60 | 53, 57, 59 | nf3an 1898 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) |
61 | | funmpt 6605 |
. . . . . . . . . . . . . 14
⊢ Fun
(𝑥 ∈ 𝐴 ↦ 𝐵) |
62 | 61 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Fun (𝑥 ∈ 𝐴 ↦ 𝐵)) |
63 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
64 | 14, 44 | dmmptd 6713 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
65 | 64 | eqcomd 2740 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 = dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
66 | 65 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 = dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
67 | 63, 66 | eleqtrd 2840 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
68 | | fvco 7006 |
. . . . . . . . . . . . 13
⊢ ((Fun
(𝑥 ∈ 𝐴 ↦ 𝐵) ∧ 𝑥 ∈ dom (𝑥 ∈ 𝐴 ↦ 𝐵)) → ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) = (𝑔‘((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
69 | 62, 67, 68 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) = (𝑔‘((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
70 | 14 | fvmpt2 7026 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
71 | 63, 44, 70 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
72 | 71 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑔‘((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) = (𝑔‘𝐵)) |
73 | 69, 72 | eqtrd 2774 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) = (𝑔‘𝐵)) |
74 | 73 | 3ad2antl1 1184 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) ∧ 𝑥 ∈ 𝐴) → ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) = (𝑔‘𝐵)) |
75 | 14 | elrnmpt1 5973 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
76 | 63, 44, 75 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
77 | 76 | 3ad2antl1 1184 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)) |
78 | | simpl3 1192 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) |
79 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → (𝑔‘𝑦) = (𝑔‘𝐵)) |
80 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵) |
81 | 79, 80 | eleq12d 2832 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → ((𝑔‘𝑦) ∈ 𝑦 ↔ (𝑔‘𝐵) ∈ 𝐵)) |
82 | 81 | rspcva 3619 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) → (𝑔‘𝐵) ∈ 𝐵) |
83 | 77, 78, 82 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑔‘𝐵) ∈ 𝐵) |
84 | 74, 83 | eqeltrd 2838 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) ∧ 𝑥 ∈ 𝐴) → ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵) |
85 | 84 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) → (𝑥 ∈ 𝐴 → ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵)) |
86 | 60, 85 | ralrimi 3254 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) → ∀𝑥 ∈ 𝐴 ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵) |
87 | 52, 86 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) → ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵)) |
88 | | fneq1 6659 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑓 Fn 𝐴 ↔ (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) Fn 𝐴)) |
89 | | nfcv 2902 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑓 |
90 | 54, 55 | nfco 5878 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
91 | 89, 90 | nfeq 2916 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑓 = (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
92 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) → (𝑓‘𝑥) = ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥)) |
93 | 92 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) → ((𝑓‘𝑥) ∈ 𝐵 ↔ ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵)) |
94 | 91, 93 | ralbid 3270 |
. . . . . . . 8
⊢ (𝑓 = (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵)) |
95 | 88, 94 | anbi12d 632 |
. . . . . . 7
⊢ (𝑓 = (𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) ↔ ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵))) |
96 | 95 | spcegv 3596 |
. . . . . 6
⊢ ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) ∈ V → (((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵)) Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 ((𝑔 ∘ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑥) ∈ 𝐵) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵))) |
97 | 42, 87, 96 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑔‘𝑦) ∈ 𝑦) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |
98 | 6, 7, 36, 97 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ (𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |
99 | 98 | ex 412 |
. . 3
⊢ (𝜑 → ((𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵))) |
100 | 99 | exlimdv 1930 |
. 2
⊢ (𝜑 → (∃𝑔(𝑔 Fn ran (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ ∀𝑦 ∈ ran (𝑥 ∈ 𝐴 ↦ 𝐵)(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵))) |
101 | 5, 100 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |