Proof of Theorem xpsfrnel
Step | Hyp | Ref
| Expression |
1 | | elixp2 7912 |
. 2
⊢ (𝐺 ∈ X𝑘 ∈
2𝑜 if(𝑘
= ∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ 𝐺 Fn 2𝑜 ∧
∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) |
2 | | 3ancoma 1045 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2𝑜 ∧
∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2𝑜 ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2𝑜
(𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) |
3 | | df2o3 7573 |
. . . . . . . 8
⊢
2𝑜 = {∅,
1𝑜} |
4 | 3 | raleqi 3142 |
. . . . . . 7
⊢
(∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ∀𝑘 ∈ {∅, 1𝑜}
(𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) |
5 | | 0ex 4790 |
. . . . . . . 8
⊢ ∅
∈ V |
6 | | 1on 7567 |
. . . . . . . . 9
⊢
1𝑜 ∈ On |
7 | 6 | elexi 3213 |
. . . . . . . 8
⊢
1𝑜 ∈ V |
8 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → (𝐺‘𝑘) = (𝐺‘∅)) |
9 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐴) |
10 | 8, 9 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑘 = ∅ → ((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘∅) ∈ 𝐴)) |
11 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑘 = 1𝑜 →
(𝐺‘𝑘) = (𝐺‘1𝑜)) |
12 | | 1n0 7575 |
. . . . . . . . . . 11
⊢
1𝑜 ≠ ∅ |
13 | | neeq1 2856 |
. . . . . . . . . . 11
⊢ (𝑘 = 1𝑜 →
(𝑘 ≠ ∅ ↔
1𝑜 ≠ ∅)) |
14 | 12, 13 | mpbiri 248 |
. . . . . . . . . 10
⊢ (𝑘 = 1𝑜 →
𝑘 ≠
∅) |
15 | | ifnefalse 4098 |
. . . . . . . . . 10
⊢ (𝑘 ≠ ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑘 = 1𝑜 →
if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) |
17 | 11, 16 | eleq12d 2695 |
. . . . . . . 8
⊢ (𝑘 = 1𝑜 →
((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘1𝑜) ∈ 𝐵)) |
18 | 5, 7, 10, 17 | ralpr 4238 |
. . . . . . 7
⊢
(∀𝑘 ∈
{∅, 1𝑜} (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵)) |
19 | 4, 18 | bitri 264 |
. . . . . 6
⊢
(∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵)) |
20 | | 2onn 7720 |
. . . . . . . . . 10
⊢
2𝑜 ∈ ω |
21 | | nnfi 8153 |
. . . . . . . . . 10
⊢
(2𝑜 ∈ ω → 2𝑜
∈ Fin) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . 9
⊢
2𝑜 ∈ Fin |
23 | | fnfi 8238 |
. . . . . . . . 9
⊢ ((𝐺 Fn 2𝑜 ∧
2𝑜 ∈ Fin) → 𝐺 ∈ Fin) |
24 | 22, 23 | mpan2 707 |
. . . . . . . 8
⊢ (𝐺 Fn 2𝑜 →
𝐺 ∈
Fin) |
25 | | elex 3212 |
. . . . . . . 8
⊢ (𝐺 ∈ Fin → 𝐺 ∈ V) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ (𝐺 Fn 2𝑜 →
𝐺 ∈
V) |
27 | 26 | biantrurd 529 |
. . . . . 6
⊢ (𝐺 Fn 2𝑜 →
(∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) |
28 | 19, 27 | syl5rbbr 275 |
. . . . 5
⊢ (𝐺 Fn 2𝑜 →
((𝐺 ∈ V ∧
∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵))) |
29 | 28 | pm5.32i 669 |
. . . 4
⊢ ((𝐺 Fn 2𝑜 ∧
(𝐺 ∈ V ∧
∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) ↔ (𝐺 Fn 2𝑜 ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵))) |
30 | | 3anass 1042 |
. . . 4
⊢ ((𝐺 Fn 2𝑜 ∧
𝐺 ∈ V ∧
∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2𝑜 ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2𝑜
(𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) |
31 | | 3anass 1042 |
. . . 4
⊢ ((𝐺 Fn 2𝑜 ∧
(𝐺‘∅) ∈
𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵) ↔ (𝐺 Fn 2𝑜 ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵))) |
32 | 29, 30, 31 | 3bitr4i 292 |
. . 3
⊢ ((𝐺 Fn 2𝑜 ∧
𝐺 ∈ V ∧
∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2𝑜 ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵)) |
33 | 2, 32 | bitri 264 |
. 2
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2𝑜 ∧
∀𝑘 ∈
2𝑜 (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2𝑜 ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵)) |
34 | 1, 33 | bitri 264 |
1
⊢ (𝐺 ∈ X𝑘 ∈
2𝑜 if(𝑘
= ∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2𝑜 ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1𝑜) ∈ 𝐵)) |