Step | Hyp | Ref
| Expression |
1 | | smfpimcc.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
2 | 1 | uzct 42611 |
. . . . . 6
⊢ 𝑍 ≼
ω |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ≼ ω) |
4 | | mptct 10294 |
. . . . 5
⊢ (𝑍 ≼ ω → (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω) |
5 | | rnct 10281 |
. . . . 5
⊢ ((𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω → ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω) |
6 | 3, 4, 5 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω) |
7 | | vex 3436 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
8 | | eqid 2738 |
. . . . . . . . 9
⊢ (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) = (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
9 | 8 | elrnmpt 5865 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ↔ ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) |
10 | 7, 9 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ↔ ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
11 | 10 | biimpi 215 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
12 | 11 | adantl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
13 | | simp3 1137 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
14 | | smfpimcc.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ SAlg) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) |
16 | | smfpimcc.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
17 | 16 | ffvelrnda 6961 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
18 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
19 | | smfpimcc.j |
. . . . . . . . . . . . 13
⊢ 𝐽 = (topGen‘ran
(,)) |
20 | | smfpimcc.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (SalGen‘𝐽) |
21 | | smfpimcc.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 ∈ 𝐵) |
23 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (◡(𝐹‘𝑚) “ 𝐴) = (◡(𝐹‘𝑚) “ 𝐴) |
24 | 15, 17, 18, 19, 20, 22, 23 | smfpimbor1 44334 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚))) |
25 | | fvex 6787 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘𝑚) ∈ V |
26 | 25 | dmex 7758 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝐹‘𝑚) ∈ V |
27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝐹‘𝑚) ∈ V) |
28 | | elrest 17138 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ SAlg ∧ dom (𝐹‘𝑚) ∈ V) → ((◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚)))) |
29 | 14, 27, 28 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚)))) |
30 | 29 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚)))) |
31 | 24, 30 | mpbid 231 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))) |
32 | | rabn0 4319 |
. . . . . . . . . . 11
⊢ ({𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅ ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))) |
33 | 31, 32 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) |
34 | 33 | 3adant3 1131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) |
35 | 13, 34 | eqnetrd 3011 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 ≠ ∅) |
36 | 35 | 3exp 1118 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ 𝑍 → (𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅))) |
37 | 36 | rexlimdv 3212 |
. . . . . 6
⊢ (𝜑 → (∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) |
38 | 37 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → (∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) |
39 | 12, 38 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → 𝑦 ≠ ∅) |
40 | 6, 39 | axccd2 42769 |
. . 3
⊢ (𝜑 → ∃𝑓∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) |
41 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑚𝜑 |
42 | | nfmpt1 5182 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
43 | 42 | nfrn 5861 |
. . . . . . . 8
⊢
Ⅎ𝑚ran
(𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
44 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑓‘𝑦) ∈ 𝑦 |
45 | 43, 44 | nfralw 3151 |
. . . . . . 7
⊢
Ⅎ𝑚∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 |
46 | 41, 45 | nfan 1902 |
. . . . . 6
⊢
Ⅎ𝑚(𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) |
47 | 1 | fvexi 6788 |
. . . . . 6
⊢ 𝑍 ∈ V |
48 | 14 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) → 𝑆 ∈ SAlg) |
49 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → (𝑓‘𝑦) = (𝑓‘𝑤)) |
50 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
51 | 49, 50 | eleq12d 2833 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → ((𝑓‘𝑦) ∈ 𝑦 ↔ (𝑓‘𝑤) ∈ 𝑤)) |
52 | 51 | rspccva 3560 |
. . . . . . 7
⊢
((∀𝑦 ∈
ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 ∧ 𝑤 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → (𝑓‘𝑤) ∈ 𝑤) |
53 | 52 | adantll 711 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) ∧ 𝑤 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → (𝑓‘𝑤) ∈ 𝑤) |
54 | | eqid 2738 |
. . . . . 6
⊢ (𝑚 ∈ 𝑍 ↦ (𝑓‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) = (𝑚 ∈ 𝑍 ↦ (𝑓‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) |
55 | 46, 47, 48, 53, 54 | smfpimcclem 44340 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)))) |
56 | 55 | ex 413 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))))) |
57 | 56 | exlimdv 1936 |
. . 3
⊢ (𝜑 → (∃𝑓∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))))) |
58 | 40, 57 | mpd 15 |
. 2
⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)))) |
59 | | smfpimcc.1 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝐹 |
60 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑚 |
61 | 59, 60 | nffv 6784 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝐹‘𝑚) |
62 | 61 | nfcnv 5787 |
. . . . . . 7
⊢
Ⅎ𝑛◡(𝐹‘𝑚) |
63 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑛𝐴 |
64 | 62, 63 | nfima 5977 |
. . . . . 6
⊢
Ⅎ𝑛(◡(𝐹‘𝑚) “ 𝐴) |
65 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑛(ℎ‘𝑚) |
66 | 61 | nfdm 5860 |
. . . . . . 7
⊢
Ⅎ𝑛dom
(𝐹‘𝑚) |
67 | 65, 66 | nfin 4150 |
. . . . . 6
⊢
Ⅎ𝑛((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) |
68 | 64, 67 | nfeq 2920 |
. . . . 5
⊢
Ⅎ𝑛(◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) |
69 | | nfv 1917 |
. . . . 5
⊢
Ⅎ𝑚(◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)) |
70 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
71 | 70 | cnveqd 5784 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ◡(𝐹‘𝑚) = ◡(𝐹‘𝑛)) |
72 | 71 | imaeq1d 5968 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (◡(𝐹‘𝑚) “ 𝐴) = (◡(𝐹‘𝑛) “ 𝐴)) |
73 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (ℎ‘𝑚) = (ℎ‘𝑛)) |
74 | 70 | dmeqd 5814 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → dom (𝐹‘𝑚) = dom (𝐹‘𝑛)) |
75 | 73, 74 | ineq12d 4147 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))) |
76 | 72, 75 | eqeq12d 2754 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) ↔ (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |
77 | 68, 69, 76 | cbvralw 3373 |
. . . 4
⊢
(∀𝑚 ∈
𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) ↔ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))) |
78 | 77 | anbi2i 623 |
. . 3
⊢ ((ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))) ↔ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |
79 | 78 | exbii 1850 |
. 2
⊢
(∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))) ↔ ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |
80 | 58, 79 | sylib 217 |
1
⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |