Proof of Theorem smflimmpt
| Step | Hyp | Ref
| Expression |
| 1 | | smflimmpt.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
| 2 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
| 3 | | smflimmpt.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
| 4 | | smflimmpt.d |
. . . . . 6
⊢ 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ } |
| 5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ }) |
| 6 | | smflimmpt.n |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑛𝜑 |
| 7 | | smflimmpt.p |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚𝜑 |
| 8 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚 𝑛 ∈ 𝑍 |
| 9 | 7, 8 | nfan 1899 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍) |
| 10 | | smflimmpt.z |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 11 | 10 | uztrn2 12897 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ 𝑍 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 12 | 11 | adantll 714 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 13 | | simpll 767 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 14 | | smflimmpt.a |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝐴 ∈ 𝑉) |
| 15 | 14 | mptexd 7244 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 16 | 13, 12, 15 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) = (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 18 | 17 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ 𝑍 ∧ (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 19 | 12, 16, 18 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 20 | 19 | dmeqd 5916 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 21 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥 𝑛 ∈ 𝑍 |
| 22 | 3, 21 | nfan 1899 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥(𝜑 ∧ 𝑛 ∈ 𝑍) |
| 23 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥 𝑚 ∈
(ℤ≥‘𝑛) |
| 24 | 22, 23 | nfan 1899 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) |
| 25 | | simplll 775 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) ∧ 𝑥 ∈ 𝐴) → 𝜑) |
| 26 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) ∧ 𝑥 ∈ 𝐴) → 𝑚 ∈ 𝑍) |
| 27 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 28 | | smflimmpt.b |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 29 | 25, 26, 27, 28 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 30 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 31 | 24, 29, 30 | fnmptd 6709 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴) |
| 32 | 31 | fndmd 6673 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = 𝐴) |
| 33 | 20, 32 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐴 = dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 34 | 9, 33 | iineq2d 5015 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 35 | 6, 34 | iuneq2df 45052 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 36 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → 𝑚 ∈ 𝑍) |
| 37 | 36, 15, 18 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 38 | 37 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) = ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 39 | 38 | dmeqd 5916 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 40 | 13, 12, 39 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → dom (𝑥 ∈ 𝐴 ↦ 𝐵) = dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 41 | 9, 40 | iineq2d 5015 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍) → ∩
𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) = ∩
𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 42 | 6, 41 | iuneq2df 45052 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) = ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)) |
| 43 | 35, 42 | eqtr4d 2780 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 = ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 44 | 43 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ↔ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵))) |
| 45 | 44 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 46 | 45 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 47 | | eliun 4995 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ↔ ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 48 | 47 | biimpi 216 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 49 | 48 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 50 | 49 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 51 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛(𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ |
| 52 | 6, 51 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝜑 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) |
| 53 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ |
| 54 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) |
| 55 | | nfcv 2905 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚𝑥 |
| 56 | | nfii1 5029 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑚∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 |
| 57 | 55, 56 | nfel 2920 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑚 𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 |
| 58 | 9, 57 | nfan 1899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑚((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 59 | 10 | eluzelz2 45414 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → 𝑛 ∈ ℤ) |
| 60 | 59 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ ℤ) |
| 61 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(ℤ≥‘𝑛) = (ℤ≥‘𝑛) |
| 62 | 10 | fvexi 6920 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑍 ∈ V |
| 63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑍 ∈ V) |
| 64 | 10 | uzssd3 45437 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ 𝑍 → (ℤ≥‘𝑛) ⊆ 𝑍) |
| 65 | 64 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (ℤ≥‘𝑛) ⊆ 𝑍) |
| 66 | | fvexd 6921 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ V) |
| 67 | | eliinid 45116 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ∩ 𝑚 ∈ (ℤ≥‘𝑛)𝐴 ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ 𝐴) |
| 68 | 67 | adantll 714 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ 𝐴) |
| 69 | 13 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 70 | 12 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 71 | 69, 70, 68, 28 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈ 𝑊) |
| 72 | 30 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 73 | 68, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 74 | 58, 60, 61, 63, 63, 65, 65, 66, 73 | climeldmeqmpt3 45704 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ((𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) |
| 75 | 74 | adantllr 719 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ((𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) |
| 76 | 54, 75 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) |
| 77 | 76 | exp31 419 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ))) |
| 78 | 52, 53, 77 | rexlimd 3266 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) |
| 79 | 78 | adantrl 716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) |
| 80 | 50, 79 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) |
| 81 | 46, 80 | jca 511 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) |
| 82 | 81 | ex 412 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ))) |
| 83 | 44 | biimpar 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵)) → 𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 84 | 83 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 85 | 84, 48 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 86 | 6, 53 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(𝜑 ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) |
| 87 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) |
| 88 | 74 | adantllr 719 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ((𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) |
| 89 | 87, 88 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) ∧ 𝑛 ∈ 𝑍) ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) |
| 90 | 89 | exp31 419 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ))) |
| 91 | 86, 51, 90 | rexlimd 3266 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) |
| 92 | 91 | adantrl 716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) |
| 93 | 85, 92 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) → (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) |
| 94 | 84, 93 | jca 511 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ )) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ )) |
| 95 | 94 | ex 412 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ) → (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ))) |
| 96 | 82, 95 | impbid 212 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∧ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ ) ↔ (𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∧ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ))) |
| 97 | 3, 96 | rabbida3 45140 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ } = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∣ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ }) |
| 98 | 5, 97 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → 𝐷 = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∣ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ }) |
| 99 | 4 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 ↔ 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ }) |
| 100 | 99 | biimpi 216 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐷 → 𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ }) |
| 101 | | rabidim1 3459 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ } → 𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 102 | 100, 101,
48 | 3syl 18 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐷 → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 103 | 102 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 104 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝑥 |
| 105 | | nfiu1 5027 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 |
| 106 | 51, 105 | nfrabw 3475 |
. . . . . . . . . 10
⊢
Ⅎ𝑛{𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)𝐴 ∣ (𝑚 ∈ 𝑍 ↦ 𝐵) ∈ dom ⇝ } |
| 107 | 4, 106 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑛𝐷 |
| 108 | 104, 107 | nfel 2920 |
. . . . . . . 8
⊢
Ⅎ𝑛 𝑥 ∈ 𝐷 |
| 109 | 6, 108 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑛(𝜑 ∧ 𝑥 ∈ 𝐷) |
| 110 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑛( ⇝
‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵)) |
| 111 | 7, 8, 57 | nf3an 1901 |
. . . . . . . . . 10
⊢
Ⅎ𝑚(𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) |
| 112 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ 𝑍) |
| 113 | 112, 59 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑛 ∈ ℤ) |
| 114 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → 𝑍 ∈ V) |
| 115 | 10, 112 | uzssd2 45428 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → (ℤ≥‘𝑛) ⊆ 𝑍) |
| 116 | | fvexd 6921 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ V) |
| 117 | 67 | 3ad2antl3 1188 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑥 ∈ 𝐴) |
| 118 | | simpl1 1192 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝜑) |
| 119 | 112, 11 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝑚 ∈ 𝑍) |
| 120 | 118, 119,
117, 28 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → 𝐵 ∈ 𝑊) |
| 121 | 117, 120,
72 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) ∧ 𝑚 ∈ (ℤ≥‘𝑛)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 122 | 111, 113,
61, 114, 114, 115, 115, 116, 121 | climfveqmpt3 45697 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ 𝑍 ∧ 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
| 123 | 122 | 3exp 1120 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵))))) |
| 124 | 123 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝑛 ∈ 𝑍 → (𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵))))) |
| 125 | 109, 110,
124 | rexlimd 3266 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (∃𝑛 ∈ 𝑍 𝑥 ∈ ∩
𝑚 ∈
(ℤ≥‘𝑛)𝐴 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵)))) |
| 126 | 103, 125 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵))) |
| 127 | 126 | eqcomd 2743 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵)) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))) |
| 128 | 3, 98, 127 | mpteq12da 5227 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐷 ↦ ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ 𝐵))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∣ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))))) |
| 129 | 38 | eqcomd 2743 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) = (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 130 | 129 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) |
| 131 | 7, 130 | mpteq2da 5240 |
. . . . . . 7
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) |
| 132 | 131 | eqcomd 2743 |
. . . . . 6
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) |
| 133 | 132 | eleq1d 2826 |
. . . . 5
⊢ (𝜑 → ((𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ ↔ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ )) |
| 134 | 3, 42, 133 | rabbida2 45137 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∣ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ } = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ }) |
| 135 | 130 | eqcomd 2743 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) |
| 136 | 7, 135 | mpteq2da 5240 |
. . . . 5
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) = (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))) |
| 137 | 136 | fveq2d 6910 |
. . . 4
⊢ (𝜑 → ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥))) = ( ⇝ ‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
| 138 | 3, 134, 137 | mpteq12df 5228 |
. . 3
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom (𝑥 ∈ 𝐴 ↦ 𝐵) ∣ (𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))))) |
| 139 | 2, 128, 138 | 3eqtrd 2781 |
. 2
⊢ (𝜑 → 𝐺 = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥))))) |
| 140 | | nfmpt1 5250 |
. . 3
⊢
Ⅎ𝑚(𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 141 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑥𝑍 |
| 142 | | nfmpt1 5250 |
. . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
| 143 | 141, 142 | nfmpt 5249 |
. . 3
⊢
Ⅎ𝑥(𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)) |
| 144 | | smflimmpt.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 145 | | smflimmpt.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 146 | | smflimmpt.l |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ 𝑍) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ (SMblFn‘𝑆)) |
| 147 | 7, 146, 17 | fmptdf 7137 |
. . 3
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵)):𝑍⟶(SMblFn‘𝑆)) |
| 148 | | eqid 2737 |
. . 3
⊢ {𝑥 ∈ ∪ 𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } = {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } |
| 149 | | eqid 2737 |
. . 3
⊢ (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) = (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) |
| 150 | 140, 143,
144, 10, 145, 147, 148, 149 | smflim2 46821 |
. 2
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ ∪
𝑛 ∈ 𝑍 ∩ 𝑚 ∈
(ℤ≥‘𝑛)dom ((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚) ∣ (𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)) ∈ dom ⇝ } ↦ ( ⇝
‘(𝑚 ∈ 𝑍 ↦ (((𝑚 ∈ 𝑍 ↦ (𝑥 ∈ 𝐴 ↦ 𝐵))‘𝑚)‘𝑥)))) ∈ (SMblFn‘𝑆)) |
| 151 | 139, 150 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝐺 ∈ (SMblFn‘𝑆)) |