Step | Hyp | Ref
| Expression |
1 | | limcrcl 24618 |
. . . . 5
⊢ (𝑥 ∈ (𝐹 limℂ 𝐶) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐶 ∈ ℂ)) |
2 | 1 | simp3d 1145 |
. . . 4
⊢ (𝑥 ∈ (𝐹 limℂ 𝐶) → 𝐶 ∈ ℂ) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐶) → 𝐶 ∈ ℂ)) |
4 | | elinel1 4083 |
. . . . 5
⊢ (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶)) |
5 | | limcrcl 24618 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) → ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ ∧ dom (𝐹 ↾ 𝐴) ⊆ ℂ ∧ 𝐶 ∈ ℂ)) |
6 | 5 | simp3d 1145 |
. . . . 5
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) → 𝐶 ∈ ℂ) |
7 | 4, 6 | syl 17 |
. . . 4
⊢ (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝐶 ∈ ℂ) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝐶 ∈ ℂ)) |
9 | | prfi 8860 |
. . . . . . . 8
⊢ {𝐴, 𝐵} ∈ Fin |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → {𝐴, 𝐵} ∈ Fin) |
11 | | limcun.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
12 | 11 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐴 ⊆ ℂ) |
13 | | limcun.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
14 | 13 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐵 ⊆ ℂ) |
15 | | cnex 10689 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
16 | 15 | ssex 5186 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℂ → 𝐴 ∈ V) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐴 ∈ V) |
18 | 15 | ssex 5186 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ ℂ → 𝐵 ∈ V) |
19 | 14, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐵 ∈ V) |
20 | | sseq1 3900 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑦 ⊆ ℂ ↔ 𝐴 ⊆ ℂ)) |
21 | | sseq1 3900 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑦 ⊆ ℂ ↔ 𝐵 ⊆ ℂ)) |
22 | 20, 21 | ralprg 4582 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑦 ∈ {𝐴, 𝐵}𝑦 ⊆ ℂ ↔ (𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ))) |
23 | 17, 19, 22 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑦 ∈ {𝐴, 𝐵}𝑦 ⊆ ℂ ↔ (𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ))) |
24 | 12, 14, 23 | mpbir2and 713 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∀𝑦 ∈ {𝐴, 𝐵}𝑦 ⊆ ℂ) |
25 | | limcun.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝐴 ∪ 𝐵)⟶ℂ) |
26 | 25 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐹:(𝐴 ∪ 𝐵)⟶ℂ) |
27 | | uniiun 4941 |
. . . . . . . . . 10
⊢ ∪ {𝐴,
𝐵} = ∪ 𝑦 ∈ {𝐴, 𝐵}𝑦 |
28 | | uniprg 4810 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) |
29 | 17, 19, 28 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) |
30 | 27, 29 | eqtr3id 2787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∪ 𝑦 ∈ {𝐴, 𝐵}𝑦 = (𝐴 ∪ 𝐵)) |
31 | 30 | feq2d 6484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐹:∪ 𝑦 ∈ {𝐴, 𝐵}𝑦⟶ℂ ↔ 𝐹:(𝐴 ∪ 𝐵)⟶ℂ)) |
32 | 26, 31 | mpbird 260 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐹:∪ 𝑦 ∈ {𝐴, 𝐵}𝑦⟶ℂ) |
33 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐶 ∈ ℂ) |
34 | 10, 24, 32, 33 | limciun 24638 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐹 limℂ 𝐶) = (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶))) |
35 | 34 | eleq2d 2818 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶)))) |
36 | | reseq2 5814 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝐹 ↾ 𝑦) = (𝐹 ↾ 𝐴)) |
37 | 36 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝐹 ↾ 𝑦) limℂ 𝐶) = ((𝐹 ↾ 𝐴) limℂ 𝐶)) |
38 | 37 | eleq2d 2818 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ 𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶))) |
39 | | reseq2 5814 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ 𝐵)) |
40 | 39 | oveq1d 7179 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐵 → ((𝐹 ↾ 𝑦) limℂ 𝐶) = ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
41 | 40 | eleq2d 2818 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
42 | 38, 41 | ralprg 4582 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
43 | 17, 19, 42 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
44 | 43 | anbi2d 632 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ ℂ ∧ ∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))))) |
45 | | limccl 24619 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝐴) limℂ 𝐶) ⊆ ℂ |
46 | 45 | sseli 3871 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) → 𝑥 ∈ ℂ) |
47 | 46 | adantr 484 |
. . . . . . . 8
⊢ ((𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑥 ∈ ℂ) |
48 | 47 | pm4.71ri 564 |
. . . . . . 7
⊢ ((𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
49 | 44, 48 | bitr4di 292 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ ℂ ∧ ∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
50 | | elriin 4963 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶))) |
51 | | elin 3857 |
. . . . . 6
⊢ (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
52 | 49, 50, 51 | 3bitr4g 317 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
53 | 35, 52 | bitrd 282 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
54 | 53 | ex 416 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ℂ → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶))))) |
55 | 3, 8, 54 | pm5.21ndd 384 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
56 | 55 | eqrdv 2736 |
1
⊢ (𝜑 → (𝐹 limℂ 𝐶) = (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |