Proof of Theorem xpsfrnel
Step | Hyp | Ref
| Expression |
1 | | elixp2 8468 |
. 2
⊢ (𝐺 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) |
2 | | 3ancoma 1094 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧
∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) |
3 | | df2o3 8120 |
. . . . . . . 8
⊢
2o = {∅, 1o} |
4 | 3 | raleqi 3416 |
. . . . . . 7
⊢
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ∀𝑘 ∈ {∅, 1o} (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) |
5 | | 0ex 5214 |
. . . . . . . 8
⊢ ∅
∈ V |
6 | | 1oex 8113 |
. . . . . . . 8
⊢
1o ∈ V |
7 | | fveq2 6673 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (𝐺‘𝑘) = (𝐺‘∅)) |
8 | | iftrue 4476 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐴) |
9 | 7, 8 | eleq12d 2910 |
. . . . . . . 8
⊢ (𝑘 = ∅ → ((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘∅) ∈ 𝐴)) |
10 | | fveq2 6673 |
. . . . . . . . 9
⊢ (𝑘 = 1o → (𝐺‘𝑘) = (𝐺‘1o)) |
11 | | 1n0 8122 |
. . . . . . . . . . 11
⊢
1o ≠ ∅ |
12 | | neeq1 3081 |
. . . . . . . . . . 11
⊢ (𝑘 = 1o → (𝑘 ≠ ∅ ↔
1o ≠ ∅)) |
13 | 11, 12 | mpbiri 260 |
. . . . . . . . . 10
⊢ (𝑘 = 1o → 𝑘 ≠ ∅) |
14 | | ifnefalse 4482 |
. . . . . . . . . 10
⊢ (𝑘 ≠ ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
15 | 13, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 = 1o → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
16 | 10, 15 | eleq12d 2910 |
. . . . . . . 8
⊢ (𝑘 = 1o → ((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘1o) ∈ 𝐵)) |
17 | 5, 6, 9, 16 | ralpr 4639 |
. . . . . . 7
⊢
(∀𝑘 ∈
{∅, 1o} (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
18 | 4, 17 | bitri 277 |
. . . . . 6
⊢
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
19 | | 2onn 8269 |
. . . . . . . . . 10
⊢
2o ∈ ω |
20 | | nnfi 8714 |
. . . . . . . . . 10
⊢
(2o ∈ ω → 2o ∈
Fin) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . 9
⊢
2o ∈ Fin |
22 | | fnfi 8799 |
. . . . . . . . 9
⊢ ((𝐺 Fn 2o ∧
2o ∈ Fin) → 𝐺 ∈ Fin) |
23 | 21, 22 | mpan2 689 |
. . . . . . . 8
⊢ (𝐺 Fn 2o → 𝐺 ∈ Fin) |
24 | 23 | elexd 3517 |
. . . . . . 7
⊢ (𝐺 Fn 2o → 𝐺 ∈ V) |
25 | 24 | biantrurd 535 |
. . . . . 6
⊢ (𝐺 Fn 2o →
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) |
26 | 18, 25 | syl5rbbr 288 |
. . . . 5
⊢ (𝐺 Fn 2o → ((𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) |
27 | 26 | pm5.32i 577 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) |
28 | | 3anass 1091 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) |
29 | | 3anass 1091 |
. . . 4
⊢ ((𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) |
30 | 27, 28, 29 | 3bitr4i 305 |
. . 3
⊢ ((𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
31 | 2, 30 | bitri 277 |
. 2
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧
∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |
32 | 1, 31 | bitri 277 |
1
⊢ (𝐺 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |