Step | Hyp | Ref
| Expression |
1 | | limcrcl 25038 |
. . . . 5
⊢ (𝑥 ∈ (𝐹 limℂ 𝐶) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐶 ∈ ℂ)) |
2 | 1 | simp3d 1143 |
. . . 4
⊢ (𝑥 ∈ (𝐹 limℂ 𝐶) → 𝐶 ∈ ℂ) |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐶) → 𝐶 ∈ ℂ)) |
4 | | elinel1 4129 |
. . . . 5
⊢ (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶)) |
5 | | limcrcl 25038 |
. . . . . 6
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) → ((𝐹 ↾ 𝐴):dom (𝐹 ↾ 𝐴)⟶ℂ ∧ dom (𝐹 ↾ 𝐴) ⊆ ℂ ∧ 𝐶 ∈ ℂ)) |
6 | 5 | simp3d 1143 |
. . . . 5
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) → 𝐶 ∈ ℂ) |
7 | 4, 6 | syl 17 |
. . . 4
⊢ (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝐶 ∈ ℂ) |
8 | 7 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝐶 ∈ ℂ)) |
9 | | prfi 9089 |
. . . . . . . 8
⊢ {𝐴, 𝐵} ∈ Fin |
10 | 9 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → {𝐴, 𝐵} ∈ Fin) |
11 | | limcun.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
12 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐴 ⊆ ℂ) |
13 | | limcun.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
14 | 13 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐵 ⊆ ℂ) |
15 | | cnex 10952 |
. . . . . . . . . . 11
⊢ ℂ
∈ V |
16 | 15 | ssex 5245 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ ℂ → 𝐴 ∈ V) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐴 ∈ V) |
18 | 15 | ssex 5245 |
. . . . . . . . . 10
⊢ (𝐵 ⊆ ℂ → 𝐵 ∈ V) |
19 | 14, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐵 ∈ V) |
20 | | sseq1 3946 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑦 ⊆ ℂ ↔ 𝐴 ⊆ ℂ)) |
21 | | sseq1 3946 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑦 ⊆ ℂ ↔ 𝐵 ⊆ ℂ)) |
22 | 20, 21 | ralprg 4630 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑦 ∈ {𝐴, 𝐵}𝑦 ⊆ ℂ ↔ (𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ))) |
23 | 17, 19, 22 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑦 ∈ {𝐴, 𝐵}𝑦 ⊆ ℂ ↔ (𝐴 ⊆ ℂ ∧ 𝐵 ⊆ ℂ))) |
24 | 12, 14, 23 | mpbir2and 710 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∀𝑦 ∈ {𝐴, 𝐵}𝑦 ⊆ ℂ) |
25 | | limcun.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(𝐴 ∪ 𝐵)⟶ℂ) |
26 | 25 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐹:(𝐴 ∪ 𝐵)⟶ℂ) |
27 | | uniiun 4988 |
. . . . . . . . . 10
⊢ ∪ {𝐴,
𝐵} = ∪ 𝑦 ∈ {𝐴, 𝐵}𝑦 |
28 | | uniprg 4856 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) |
29 | 17, 19, 28 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∪ {𝐴,
𝐵} = (𝐴 ∪ 𝐵)) |
30 | 27, 29 | eqtr3id 2792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ∪ 𝑦 ∈ {𝐴, 𝐵}𝑦 = (𝐴 ∪ 𝐵)) |
31 | 30 | feq2d 6586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐹:∪ 𝑦 ∈ {𝐴, 𝐵}𝑦⟶ℂ ↔ 𝐹:(𝐴 ∪ 𝐵)⟶ℂ)) |
32 | 26, 31 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐹:∪ 𝑦 ∈ {𝐴, 𝐵}𝑦⟶ℂ) |
33 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → 𝐶 ∈ ℂ) |
34 | 10, 24, 32, 33 | limciun 25058 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝐹 limℂ 𝐶) = (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶))) |
35 | 34 | eleq2d 2824 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶)))) |
36 | | reseq2 5886 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 → (𝐹 ↾ 𝑦) = (𝐹 ↾ 𝐴)) |
37 | 36 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐴 → ((𝐹 ↾ 𝑦) limℂ 𝐶) = ((𝐹 ↾ 𝐴) limℂ 𝐶)) |
38 | 37 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐴 → (𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ 𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶))) |
39 | | reseq2 5886 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐵 → (𝐹 ↾ 𝑦) = (𝐹 ↾ 𝐵)) |
40 | 39 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝐵 → ((𝐹 ↾ 𝑦) limℂ 𝐶) = ((𝐹 ↾ 𝐵) limℂ 𝐶)) |
41 | 40 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝑦 = 𝐵 → (𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
42 | 38, 41 | ralprg 4630 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
43 | 17, 19, 42 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
44 | 43 | anbi2d 629 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ ℂ ∧ ∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))))) |
45 | | limccl 25039 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ 𝐴) limℂ 𝐶) ⊆ ℂ |
46 | 45 | sseli 3917 |
. . . . . . . . 9
⊢ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) → 𝑥 ∈ ℂ) |
47 | 46 | adantr 481 |
. . . . . . . 8
⊢ ((𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) → 𝑥 ∈ ℂ) |
48 | 47 | pm4.71ri 561 |
. . . . . . 7
⊢ ((𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
49 | 44, 48 | bitr4di 289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ ℂ ∧ ∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
50 | | elriin 5010 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ (𝑥 ∈ ℂ ∧ ∀𝑦 ∈ {𝐴, 𝐵}𝑥 ∈ ((𝐹 ↾ 𝑦) limℂ 𝐶))) |
51 | | elin 3903 |
. . . . . 6
⊢ (𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)) ↔ (𝑥 ∈ ((𝐹 ↾ 𝐴) limℂ 𝐶) ∧ 𝑥 ∈ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |
52 | 49, 50, 51 | 3bitr4g 314 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ (ℂ ∩ ∩ 𝑦 ∈ {𝐴, 𝐵} ((𝐹 ↾ 𝑦) limℂ 𝐶)) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
53 | 35, 52 | bitrd 278 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ ℂ) → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
54 | 53 | ex 413 |
. . 3
⊢ (𝜑 → (𝐶 ∈ ℂ → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶))))) |
55 | 3, 8, 54 | pm5.21ndd 381 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐹 limℂ 𝐶) ↔ 𝑥 ∈ (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶)))) |
56 | 55 | eqrdv 2736 |
1
⊢ (𝜑 → (𝐹 limℂ 𝐶) = (((𝐹 ↾ 𝐴) limℂ 𝐶) ∩ ((𝐹 ↾ 𝐵) limℂ 𝐶))) |