Proof of Theorem bj-charfundcALT
Step | Hyp | Ref
| Expression |
1 | | bj-charfundc.1 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅))) |
2 | 1 | bj-charfun 13369 |
. 2
⊢ (𝜑 → ((𝐹:𝑋⟶𝒫 1o ∧ (𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))):((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))⟶2o) ∧
(∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅))) |
3 | | difin 3344 |
. . . . . . . . . . . 12
⊢ (𝑋 ∖ (𝑋 ∩ 𝐴)) = (𝑋 ∖ 𝐴) |
4 | 3 | eqcomi 2161 |
. . . . . . . . . . 11
⊢ (𝑋 ∖ 𝐴) = (𝑋 ∖ (𝑋 ∩ 𝐴)) |
5 | 4 | a1i 9 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∖ 𝐴) = (𝑋 ∖ (𝑋 ∩ 𝐴))) |
6 | 5 | uneq2d 3261 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴)) = ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ (𝑋 ∩ 𝐴)))) |
7 | | inss1 3327 |
. . . . . . . . . . 11
⊢ (𝑋 ∩ 𝐴) ⊆ 𝑋 |
8 | 7 | a1i 9 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 ∩ 𝐴) ⊆ 𝑋) |
9 | | bj-charfundc.dc |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ 𝐴) |
10 | | elin 3290 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝑋 ∩ 𝐴) ↔ (𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝐴)) |
11 | 10 | baibr 906 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑋 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ (𝑋 ∩ 𝐴))) |
12 | 11 | dcbid 824 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑋 → (DECID 𝑥 ∈ 𝐴 ↔ DECID 𝑥 ∈ (𝑋 ∩ 𝐴))) |
13 | 12 | ralbiia 2471 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
𝑋 DECID
𝑥 ∈ 𝐴 ↔ ∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ (𝑋 ∩ 𝐴)) |
14 | 9, 13 | sylib 121 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ (𝑋 ∩ 𝐴)) |
15 | | undifdcss 6864 |
. . . . . . . . . 10
⊢ (𝑋 = ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ (𝑋 ∩ 𝐴))) ↔ ((𝑋 ∩ 𝐴) ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑋 DECID 𝑥 ∈ (𝑋 ∩ 𝐴))) |
16 | 8, 14, 15 | sylanbrc 414 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 = ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ (𝑋 ∩ 𝐴)))) |
17 | 6, 16 | eqtr4d 2193 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴)) = 𝑋) |
18 | 17 | reseq2d 4865 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))) = (𝐹 ↾ 𝑋)) |
19 | | ssidd 3149 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ⊆ 𝑋) |
20 | 19 | resmptd 4916 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅)) ↾ 𝑋) = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅))) |
21 | 1 | reseq1d 4864 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ 𝑋) = ((𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ 𝐴, 1o, ∅)) ↾ 𝑋)) |
22 | 20, 21, 1 | 3eqtr4d 2200 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝑋) = 𝐹) |
23 | 18, 22 | eqtrd 2190 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))) = 𝐹) |
24 | 23, 17 | feq12d 5308 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))):((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))⟶2o ↔ 𝐹:𝑋⟶2o)) |
25 | 24 | biimpd 143 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))):((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))⟶2o → 𝐹:𝑋⟶2o)) |
26 | 25 | adantld 276 |
. . 3
⊢ (𝜑 → ((𝐹:𝑋⟶𝒫 1o ∧ (𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))):((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))⟶2o) → 𝐹:𝑋⟶2o)) |
27 | 26 | anim1d 334 |
. 2
⊢ (𝜑 → (((𝐹:𝑋⟶𝒫 1o ∧ (𝐹 ↾ ((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))):((𝑋 ∩ 𝐴) ∪ (𝑋 ∖ 𝐴))⟶2o) ∧
(∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅)) → (𝐹:𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅)))) |
28 | 2, 27 | mpd 13 |
1
⊢ (𝜑 → (𝐹:𝑋⟶2o ∧ (∀𝑥 ∈ (𝑋 ∩ 𝐴)(𝐹‘𝑥) = 1o ∧ ∀𝑥 ∈ (𝑋 ∖ 𝐴)(𝐹‘𝑥) = ∅))) |