| Step | Hyp | Ref
| Expression |
| 1 | | smfpimcc.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 2 | 1 | uzct 45068 |
. . . . . 6
⊢ 𝑍 ≼
ω |
| 3 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ≼ ω) |
| 4 | | mptct 10578 |
. . . . 5
⊢ (𝑍 ≼ ω → (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω) |
| 5 | | rnct 10565 |
. . . . 5
⊢ ((𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω → ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω) |
| 6 | 3, 4, 5 | 3syl 18 |
. . . 4
⊢ (𝜑 → ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ≼ ω) |
| 7 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 8 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) = (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 9 | 8 | elrnmpt 5969 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ↔ ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) |
| 10 | 7, 9 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) ↔ ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 11 | 10 | biimpi 216 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 12 | 11 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → ∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 13 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 14 | | smfpimcc.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑆 ∈ SAlg) |
| 16 | | smfpimcc.f |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑍⟶(SMblFn‘𝑆)) |
| 17 | 16 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝐹‘𝑚) ∈ (SMblFn‘𝑆)) |
| 18 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ dom
(𝐹‘𝑚) = dom (𝐹‘𝑚) |
| 19 | | smfpimcc.j |
. . . . . . . . . . . . 13
⊢ 𝐽 = (topGen‘ran
(,)) |
| 20 | | smfpimcc.b |
. . . . . . . . . . . . 13
⊢ 𝐵 = (SalGen‘𝐽) |
| 21 | | smfpimcc.a |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 ∈ 𝐵) |
| 23 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (◡(𝐹‘𝑚) “ 𝐴) = (◡(𝐹‘𝑚) “ 𝐴) |
| 24 | 15, 17, 18, 19, 20, 22, 23 | smfpimbor1 46815 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚))) |
| 25 | | fvex 6919 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹‘𝑚) ∈ V |
| 26 | 25 | dmex 7931 |
. . . . . . . . . . . . . . 15
⊢ dom
(𝐹‘𝑚) ∈ V |
| 27 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom (𝐹‘𝑚) ∈ V) |
| 28 | | elrest 17472 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ SAlg ∧ dom (𝐹‘𝑚) ∈ V) → ((◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚)))) |
| 29 | 14, 27, 28 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚)))) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((◡(𝐹‘𝑚) “ 𝐴) ∈ (𝑆 ↾t dom (𝐹‘𝑚)) ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚)))) |
| 31 | 24, 30 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))) |
| 32 | | rabn0 4389 |
. . . . . . . . . . 11
⊢ ({𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅ ↔ ∃𝑠 ∈ 𝑆 (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))) |
| 33 | 31, 32 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) |
| 34 | 33 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} ≠ ∅) |
| 35 | 13, 34 | eqnetrd 3008 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) → 𝑦 ≠ ∅) |
| 36 | 35 | 3exp 1120 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ 𝑍 → (𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅))) |
| 37 | 36 | rexlimdv 3153 |
. . . . . 6
⊢ (𝜑 → (∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) |
| 38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → (∃𝑚 ∈ 𝑍 𝑦 = {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))} → 𝑦 ≠ ∅)) |
| 39 | 12, 38 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → 𝑦 ≠ ∅) |
| 40 | 6, 39 | axccd2 45235 |
. . 3
⊢ (𝜑 → ∃𝑓∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) |
| 41 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑚𝜑 |
| 42 | | nfmpt1 5250 |
. . . . . . . . 9
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 43 | 42 | nfrn 5963 |
. . . . . . . 8
⊢
Ⅎ𝑚ran
(𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))}) |
| 44 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑚(𝑓‘𝑦) ∈ 𝑦 |
| 45 | 43, 44 | nfralw 3311 |
. . . . . . 7
⊢
Ⅎ𝑚∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 |
| 46 | 41, 45 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑚(𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) |
| 47 | 1 | fvexi 6920 |
. . . . . 6
⊢ 𝑍 ∈ V |
| 48 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) → 𝑆 ∈ SAlg) |
| 49 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → (𝑓‘𝑦) = (𝑓‘𝑤)) |
| 50 | | id 22 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → 𝑦 = 𝑤) |
| 51 | 49, 50 | eleq12d 2835 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → ((𝑓‘𝑦) ∈ 𝑦 ↔ (𝑓‘𝑤) ∈ 𝑤)) |
| 52 | 51 | rspccva 3621 |
. . . . . . 7
⊢
((∀𝑦 ∈
ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 ∧ 𝑤 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → (𝑓‘𝑤) ∈ 𝑤) |
| 53 | 52 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) ∧ 𝑤 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) → (𝑓‘𝑤) ∈ 𝑤) |
| 54 | | eqid 2737 |
. . . . . 6
⊢ (𝑚 ∈ 𝑍 ↦ (𝑓‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) = (𝑚 ∈ 𝑍 ↦ (𝑓‘{𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})) |
| 55 | 46, 47, 48, 53, 54 | smfpimcclem 46822 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦) → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)))) |
| 56 | 55 | ex 412 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))))) |
| 57 | 56 | exlimdv 1933 |
. . 3
⊢ (𝜑 → (∃𝑓∀𝑦 ∈ ran (𝑚 ∈ 𝑍 ↦ {𝑠 ∈ 𝑆 ∣ (◡(𝐹‘𝑚) “ 𝐴) = (𝑠 ∩ dom (𝐹‘𝑚))})(𝑓‘𝑦) ∈ 𝑦 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))))) |
| 58 | 40, 57 | mpd 15 |
. 2
⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)))) |
| 59 | | smfpimcc.1 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝐹 |
| 60 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑚 |
| 61 | 59, 60 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝐹‘𝑚) |
| 62 | 61 | nfcnv 5889 |
. . . . . . 7
⊢
Ⅎ𝑛◡(𝐹‘𝑚) |
| 63 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑛𝐴 |
| 64 | 62, 63 | nfima 6086 |
. . . . . 6
⊢
Ⅎ𝑛(◡(𝐹‘𝑚) “ 𝐴) |
| 65 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑛(ℎ‘𝑚) |
| 66 | 61 | nfdm 5962 |
. . . . . . 7
⊢
Ⅎ𝑛dom
(𝐹‘𝑚) |
| 67 | 65, 66 | nfin 4224 |
. . . . . 6
⊢
Ⅎ𝑛((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) |
| 68 | 64, 67 | nfeq 2919 |
. . . . 5
⊢
Ⅎ𝑛(◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) |
| 69 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑚(◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)) |
| 70 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
| 71 | 70 | cnveqd 5886 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ◡(𝐹‘𝑚) = ◡(𝐹‘𝑛)) |
| 72 | 71 | imaeq1d 6077 |
. . . . . 6
⊢ (𝑚 = 𝑛 → (◡(𝐹‘𝑚) “ 𝐴) = (◡(𝐹‘𝑛) “ 𝐴)) |
| 73 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (ℎ‘𝑚) = (ℎ‘𝑛)) |
| 74 | 70 | dmeqd 5916 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → dom (𝐹‘𝑚) = dom (𝐹‘𝑛)) |
| 75 | 73, 74 | ineq12d 4221 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))) |
| 76 | 72, 75 | eqeq12d 2753 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) ↔ (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |
| 77 | 68, 69, 76 | cbvralw 3306 |
. . . 4
⊢
(∀𝑚 ∈
𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚)) ↔ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛))) |
| 78 | 77 | anbi2i 623 |
. . 3
⊢ ((ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))) ↔ (ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |
| 79 | 78 | exbii 1848 |
. 2
⊢
(∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑚 ∈ 𝑍 (◡(𝐹‘𝑚) “ 𝐴) = ((ℎ‘𝑚) ∩ dom (𝐹‘𝑚))) ↔ ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |
| 80 | 58, 79 | sylib 218 |
1
⊢ (𝜑 → ∃ℎ(ℎ:𝑍⟶𝑆 ∧ ∀𝑛 ∈ 𝑍 (◡(𝐹‘𝑛) “ 𝐴) = ((ℎ‘𝑛) ∩ dom (𝐹‘𝑛)))) |