Proof of Theorem xpsfrnel2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | xpsfrnel 17607 | . 2
⊢
({〈∅, 𝑋〉, 〈1o, 𝑌〉} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ ({〈∅, 𝑋〉, 〈1o,
𝑌〉} Fn 2o
∧ ({〈∅, 𝑋〉, 〈1o, 𝑌〉}‘∅) ∈
𝐴 ∧ ({〈∅,
𝑋〉,
〈1o, 𝑌〉}‘1o) ∈ 𝐵)) | 
| 2 |  | fnpr2ob 17603 | . . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) ↔
{〈∅, 𝑋〉,
〈1o, 𝑌〉} Fn 2o) | 
| 3 | 2 | biimpri 228 | . . . 4
⊢
({〈∅, 𝑋〉, 〈1o, 𝑌〉} Fn 2o →
(𝑋 ∈ V ∧ 𝑌 ∈ V)) | 
| 4 | 3 | 3ad2ant1 1134 | . . 3
⊢
(({〈∅, 𝑋〉, 〈1o, 𝑌〉} Fn 2o ∧
({〈∅, 𝑋〉,
〈1o, 𝑌〉}‘∅) ∈ 𝐴 ∧ ({〈∅, 𝑋〉, 〈1o,
𝑌〉}‘1o) ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | 
| 5 |  | elex 3501 | . . . 4
⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ V) | 
| 6 |  | elex 3501 | . . . 4
⊢ (𝑌 ∈ 𝐵 → 𝑌 ∈ V) | 
| 7 | 5, 6 | anim12i 613 | . . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | 
| 8 |  | 3anass 1095 | . . . 4
⊢
(({〈∅, 𝑋〉, 〈1o, 𝑌〉} Fn 2o ∧
({〈∅, 𝑋〉,
〈1o, 𝑌〉}‘∅) ∈ 𝐴 ∧ ({〈∅, 𝑋〉, 〈1o,
𝑌〉}‘1o) ∈ 𝐵) ↔ ({〈∅, 𝑋〉, 〈1o,
𝑌〉} Fn 2o
∧ (({〈∅, 𝑋〉, 〈1o, 𝑌〉}‘∅) ∈
𝐴 ∧ ({〈∅,
𝑋〉,
〈1o, 𝑌〉}‘1o) ∈ 𝐵))) | 
| 9 |  | fnpr2o 17602 | . . . . . 6
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) →
{〈∅, 𝑋〉,
〈1o, 𝑌〉} Fn 2o) | 
| 10 | 9 | biantrurd 532 | . . . . 5
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) →
((({〈∅, 𝑋〉,
〈1o, 𝑌〉}‘∅) ∈ 𝐴 ∧ ({〈∅, 𝑋〉, 〈1o,
𝑌〉}‘1o) ∈ 𝐵) ↔ ({〈∅, 𝑋〉, 〈1o,
𝑌〉} Fn 2o
∧ (({〈∅, 𝑋〉, 〈1o, 𝑌〉}‘∅) ∈
𝐴 ∧ ({〈∅,
𝑋〉,
〈1o, 𝑌〉}‘1o) ∈ 𝐵)))) | 
| 11 |  | fvpr0o 17604 | . . . . . . 7
⊢ (𝑋 ∈ V →
({〈∅, 𝑋〉,
〈1o, 𝑌〉}‘∅) = 𝑋) | 
| 12 | 11 | eleq1d 2826 | . . . . . 6
⊢ (𝑋 ∈ V →
(({〈∅, 𝑋〉,
〈1o, 𝑌〉}‘∅) ∈ 𝐴 ↔ 𝑋 ∈ 𝐴)) | 
| 13 |  | fvpr1o 17605 | . . . . . . 7
⊢ (𝑌 ∈ V →
({〈∅, 𝑋〉,
〈1o, 𝑌〉}‘1o) = 𝑌) | 
| 14 | 13 | eleq1d 2826 | . . . . . 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 378 | . 2
⊢
(({〈∅, 𝑋〉, 〈1o, 𝑌〉} Fn 2o ∧
({〈∅, 𝑋〉,
〈1o, 𝑌〉}‘∅) ∈ 𝐴 ∧ ({〈∅, 𝑋〉, 〈1o,
𝑌〉}‘1o) ∈ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) | 
| 19 | 1, 18 | bitri 275 | 1
⊢
({〈∅, 𝑋〉, 〈1o, 𝑌〉} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵)) |