Proof of Theorem xpsfrnel
Step | Hyp | Ref
| Expression |
1 | | elixp2 8178 |
. 2
⊢ (𝐺 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) |
2 | | 3ancoma 1125 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧
∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) |
3 | | df2o3 7839 |
. . . . . . . 8
⊢
2o = {∅, 1o} |
4 | 3 | raleqi 3353 |
. . . . . . 7
⊢
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ∀𝑘 ∈ {∅, 1o} (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) |
5 | | 0ex 5013 |
. . . . . . . 8
⊢ ∅
∈ V |
6 | | 1oex 7833 |
. . . . . . . 8
⊢
1o ∈ V |
7 | | fveq2 6432 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (𝐺‘𝑘) = (𝐺‘∅)) |
8 | | iftrue 4311 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐴) |
9 | 7, 8 | eleq12d 2899 |
. . . . . . . 8
⊢ (𝑘 = ∅ → ((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘∅) ∈ 𝐴)) |
10 | | fveq2 6432 |
. . . . . . . . 9
⊢ (𝑘 = 1o → (𝐺‘𝑘) = (𝐺‘1o)) |
11 | | 1n0 7841 |
. . . . . . . . . . 11
⊢
1o ≠ ∅ |
12 | | neeq1 3060 |
. . . . . . . . . . 11
⊢ (𝑘 = 1o → (𝑘 ≠ ∅ ↔
1o ≠ ∅)) |
13 | 11, 12 | mpbiri 250 |
. . . . . . . . . 10
⊢ (𝑘 = 1o → 𝑘 ≠ ∅) |
14 | | ifnefalse 4317 |
. . . . . . . . . 10
⊢ (𝑘 ≠ ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 = 1o → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
16 | 10, 15 | eleq12d 2899 |
. . . . . . . 8
⊢ (𝑘 = 1o → ((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘1o) ∈ 𝐵)) |
17 | 5, 6, 9, 16 | ralpr 4456 |
. . . . . . 7
⊢
(∀𝑘 ∈
{∅, 1o} (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
18 | 4, 17 | bitri 267 |
. . . . . 6
⊢
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
19 | | 2onn 7986 |
. . . . . . . . . 10
⊢
2o ∈ ω |
20 | | nnfi 8421 |
. . . . . . . . . 10
⊢
(2o ∈ ω → 2o ∈
Fin) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . 9
⊢
2o ∈ Fin |
22 | | fnfi 8506 |
. . . . . . . . 9
⊢ ((𝐺 Fn 2o ∧
2o ∈ Fin) → 𝐺 ∈ Fin) |
23 | 21, 22 | mpan2 684 |
. . . . . . . 8
⊢ (𝐺 Fn 2o → 𝐺 ∈ Fin) |
24 | | elex 3428 |
. . . . . . . 8
⊢ (𝐺 ∈ Fin → 𝐺 ∈ V) |
25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ (𝐺 Fn 2o → 𝐺 ∈ V) |
26 | 25 | biantrurd 530 |
. . . . . 6
⊢ (𝐺 Fn 2o →
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) |
27 | 18, 26 | syl5rbbr 278 |
. . . . 5
⊢ (𝐺 Fn 2o → ((𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) |
28 | 27 | pm5.32i 572 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) |
29 | | 3anass 1122 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) |
30 | | 3anass 1122 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) |
31 | 28, 29, 30 | 3bitr4i 295 |
. . 3
⊢ ((𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
32 | 2, 31 | bitri 267 |
. 2
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧
∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
33 | 1, 32 | bitri 267 |
1
⊢ (𝐺 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |