Step | Hyp | Ref
| Expression |
1 | | xpsfrnel 17445 |
. 2
⊢
({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩} Fn 2o
∧ ({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩}‘∅) ∈
𝐴 ∧ ({⟨∅,
𝑋⟩,
⟨1o, 𝑌⟩}‘1o) ∈ 𝐵)) |
2 | | fnpr2ob 17441 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) ↔
{⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩} Fn 2o) |
3 | 2 | biimpri 227 |
. . . 4
⊢
({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} Fn 2o →
(𝑋 ∈ V ∧ 𝑌 ∈ V)) |
4 | 3 | 3ad2ant1 1134 |
. . 3
⊢
(({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} Fn 2o ∧
({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ∧ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩}‘1o) ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
5 | | elex 3464 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V) |
6 | | elex 3464 |
. . . 4
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ V) |
7 | 5, 6 | anim12i 614 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) |
8 | | 3anass 1096 |
. . . 4
⊢
(({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} Fn 2o ∧
({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ∧ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩}‘1o) ∈ 𝐵) ↔ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩} Fn 2o
∧ (({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩}‘∅) ∈
𝐴 ∧ ({⟨∅,
𝑋⟩,
⟨1o, 𝑌⟩}‘1o) ∈ 𝐵))) |
9 | | fnpr2o 17440 |
. . . . . 6
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) →
{⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩} Fn 2o) |
10 | 9 | biantrurd 534 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) →
((({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ∧ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩}‘1o) ∈ 𝐵) ↔ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩} Fn 2o
∧ (({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩}‘∅) ∈
𝐴 ∧ ({⟨∅,
𝑋⟩,
⟨1o, 𝑌⟩}‘1o) ∈ 𝐵)))) |
11 | | fvpr0o 17442 |
. . . . . . 7
⊢ (𝑋 ∈ V →
({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) = 𝑋) |
12 | 11 | eleq1d 2823 |
. . . . . 6
⊢ (𝑋 ∈ V →
(({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ↔ 𝑋 ∈ 𝐴)) |
13 | | fvpr1o 17443 |
. . . . . . 7
⊢ (𝑌 ∈ V →
({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘1o) = 𝑌) |
14 | 13 | eleq1d 2823 |
. . . . . 6
⊢ (𝑌 ∈ V →
(({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘1o) ∈ 𝐵 ↔ 𝑌 ∈ 𝐵)) |
15 | 12, 14 | bi2anan9 638 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) →
((({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ∧ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩}‘1o) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
16 | 10, 15 | bitr3d 281 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) →
(({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩} Fn 2o ∧
(({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ∧ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩}‘1o) ∈ 𝐵)) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
17 | 8, 16 | bitrid 283 |
. . 3
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) →
(({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩} Fn 2o ∧
({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ∧ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩}‘1o) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵))) |
18 | 4, 7, 17 | pm5.21nii 380 |
. 2
⊢
(({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} Fn 2o ∧
({⟨∅, 𝑋⟩,
⟨1o, 𝑌⟩}‘∅) ∈ 𝐴 ∧ ({⟨∅, 𝑋⟩, ⟨1o,
𝑌⟩}‘1o) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) |
19 | 1, 18 | bitri 275 |
1
⊢
({⟨∅, 𝑋⟩, ⟨1o, 𝑌⟩} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) |