Proof of Theorem xpsfrnel
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elixp2 8942 | . 2
⊢ (𝐺 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ 𝐺 Fn 2o ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) | 
| 2 |  | 3ancoma 1097 | . . 3
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧
∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) | 
| 3 |  | 2onn 8681 | . . . . . . . . . 10
⊢
2o ∈ ω | 
| 4 |  | nnfi 9208 | . . . . . . . . . 10
⊢
(2o ∈ ω → 2o ∈
Fin) | 
| 5 | 3, 4 | ax-mp 5 | . . . . . . . . 9
⊢
2o ∈ Fin | 
| 6 |  | fnfi 9219 | . . . . . . . . 9
⊢ ((𝐺 Fn 2o ∧
2o ∈ Fin) → 𝐺 ∈ Fin) | 
| 7 | 5, 6 | mpan2 691 | . . . . . . . 8
⊢ (𝐺 Fn 2o → 𝐺 ∈ Fin) | 
| 8 | 7 | elexd 3503 | . . . . . . 7
⊢ (𝐺 Fn 2o → 𝐺 ∈ V) | 
| 9 | 8 | biantrurd 532 | . . . . . 6
⊢ (𝐺 Fn 2o →
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) | 
| 10 |  | df2o3 8515 | . . . . . . . 8
⊢
2o = {∅, 1o} | 
| 11 | 10 | raleqi 3323 | . . . . . . 7
⊢
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ∀𝑘 ∈ {∅, 1o} (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) | 
| 12 |  | 0ex 5306 | . . . . . . . 8
⊢ ∅
∈ V | 
| 13 |  | 1oex 8517 | . . . . . . . 8
⊢
1o ∈ V | 
| 14 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑘 = ∅ → (𝐺‘𝑘) = (𝐺‘∅)) | 
| 15 |  | iftrue 4530 | . . . . . . . . 9
⊢ (𝑘 = ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐴) | 
| 16 | 14, 15 | eleq12d 2834 | . . . . . . . 8
⊢ (𝑘 = ∅ → ((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘∅) ∈ 𝐴)) | 
| 17 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑘 = 1o → (𝐺‘𝑘) = (𝐺‘1o)) | 
| 18 |  | 1n0 8527 | . . . . . . . . . . 11
⊢
1o ≠ ∅ | 
| 19 |  | neeq1 3002 | . . . . . . . . . . 11
⊢ (𝑘 = 1o → (𝑘 ≠ ∅ ↔
1o ≠ ∅)) | 
| 20 | 18, 19 | mpbiri 258 | . . . . . . . . . 10
⊢ (𝑘 = 1o → 𝑘 ≠ ∅) | 
| 21 |  | ifnefalse 4536 | . . . . . . . . . 10
⊢ (𝑘 ≠ ∅ → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) | 
| 22 | 20, 21 | syl 17 | . . . . . . . . 9
⊢ (𝑘 = 1o → if(𝑘 = ∅, 𝐴, 𝐵) = 𝐵) | 
| 23 | 17, 22 | eleq12d 2834 | . . . . . . . 8
⊢ (𝑘 = 1o → ((𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐺‘1o) ∈ 𝐵)) | 
| 24 | 12, 13, 16, 23 | ralpr 4699 | . . . . . . 7
⊢
(∀𝑘 ∈
{∅, 1o} (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) | 
| 25 | 11, 24 | bitri 275 | . . . . . 6
⊢
(∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) | 
| 26 | 9, 25 | bitr3di 286 | . . . . 5
⊢ (𝐺 Fn 2o → ((𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) | 
| 27 | 26 | pm5.32i 574 | . . . 4
⊢ ((𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵))) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) | 
| 28 |  | 3anass 1094 | . . . 4
⊢ ((𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)))) | 
| 29 |  | 3anass 1094 | . . . 4
⊢ ((𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵) ↔ (𝐺 Fn 2o ∧ ((𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵))) | 
| 30 | 27, 28, 29 | 3bitr4i 303 | . . 3
⊢ ((𝐺 Fn 2o ∧ 𝐺 ∈ V ∧ ∀𝑘 ∈ 2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) | 
| 31 | 2, 30 | bitri 275 | . 2
⊢ ((𝐺 ∈ V ∧ 𝐺 Fn 2o ∧
∀𝑘 ∈
2o (𝐺‘𝑘) ∈ if(𝑘 = ∅, 𝐴, 𝐵)) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) | 
| 32 | 1, 31 | bitri 275 | 1
⊢ (𝐺 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐺 Fn 2o ∧ (𝐺‘∅) ∈ 𝐴 ∧ (𝐺‘1o) ∈ 𝐵)) |