Proof of Theorem eliunxp2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relxp 5703 | . . . . . . . 8
⊢ Rel
(𝐴 × {𝑦}) | 
| 2 | 1 | rgenw 3065 | . . . . . . 7
⊢
∀𝑦 ∈
𝐵 Rel (𝐴 × {𝑦}) | 
| 3 |  | reliun 5826 | . . . . . . 7
⊢ (Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∀𝑦 ∈ 𝐵 Rel (𝐴 × {𝑦})) | 
| 4 | 2, 3 | mpbir 231 | . . . . . 6
⊢ Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) | 
| 5 |  | elrel 5808 | . . . . . 6
⊢ ((Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) | 
| 6 | 4, 5 | mpan 690 | . . . . 5
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) | 
| 7 |  | excom 2162 | . . . . 5
⊢
(∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) | 
| 8 | 6, 7 | sylibr 234 | . . . 4
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉) | 
| 9 | 8 | pm4.71ri 560 | . . 3
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) | 
| 10 |  | nfiu1 5027 | . . . . 5
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) | 
| 11 | 10 | nfel2 2924 | . . . 4
⊢
Ⅎ𝑦 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) | 
| 12 | 11 | 19.41 2235 | . . 3
⊢
(∃𝑦(∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) | 
| 13 |  | 19.41v 1949 | . . . . 5
⊢
(∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) | 
| 14 |  | eleq1 2829 | . . . . . . . 8
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ 〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) | 
| 15 |  | opeliun2xp 5753 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) | 
| 16 | 15 | biancomi 462 | . . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) | 
| 17 | 14, 16 | bitrdi 287 | . . . . . . 7
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 18 | 17 | pm5.32i 574 | . . . . . 6
⊢ ((𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 19 | 18 | exbii 1848 | . . . . 5
⊢
(∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 20 | 13, 19 | bitr3i 277 | . . . 4
⊢
((∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 21 | 20 | exbii 1848 | . . 3
⊢
(∃𝑦(∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 22 | 9, 12, 21 | 3bitr2i 299 | . 2
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 23 |  | excom 2162 | . 2
⊢
(∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) | 
| 24 | 22, 23 | bitri 275 | 1
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |