Step | Hyp | Ref
| Expression |
1 | | marypha2lem.t |
. 2
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) |
2 | | sneq 4601 |
. . . 4
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
3 | | fveq2 6847 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
4 | 2, 3 | xpeq12d 5669 |
. . 3
⊢ (𝑥 = 𝑧 → ({𝑥} × (𝐹‘𝑥)) = ({𝑧} × (𝐹‘𝑧))) |
5 | 4 | cbviunv 5005 |
. 2
⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × (𝐹‘𝑥)) = ∪
𝑧 ∈ 𝐴 ({𝑧} × (𝐹‘𝑧)) |
6 | | df-xp 5644 |
. . . . 5
⊢ ({𝑧} × (𝐹‘𝑧)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧))} |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝑧 ∈ 𝐴 → ({𝑧} × (𝐹‘𝑧)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧))}) |
8 | 7 | iuneq2i 4980 |
. . 3
⊢ ∪ 𝑧 ∈ 𝐴 ({𝑧} × (𝐹‘𝑧)) = ∪
𝑧 ∈ 𝐴 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧))} |
9 | | iunopab 5521 |
. . 3
⊢ ∪ 𝑧 ∈ 𝐴 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧))} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧))} |
10 | | velsn 4607 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑧} ↔ 𝑥 = 𝑧) |
11 | | equcom 2022 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
12 | 10, 11 | bitri 275 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑧} ↔ 𝑧 = 𝑥) |
13 | 12 | anbi1i 625 |
. . . . . 6
⊢ ((𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧)) ↔ (𝑧 = 𝑥 ∧ 𝑦 ∈ (𝐹‘𝑧))) |
14 | 13 | rexbii 3098 |
. . . . 5
⊢
(∃𝑧 ∈
𝐴 (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧)) ↔ ∃𝑧 ∈ 𝐴 (𝑧 = 𝑥 ∧ 𝑦 ∈ (𝐹‘𝑧))) |
15 | | fveq2 6847 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) |
16 | 15 | eleq2d 2824 |
. . . . . 6
⊢ (𝑧 = 𝑥 → (𝑦 ∈ (𝐹‘𝑧) ↔ 𝑦 ∈ (𝐹‘𝑥))) |
17 | 16 | ceqsrexbv 3611 |
. . . . 5
⊢
(∃𝑧 ∈
𝐴 (𝑧 = 𝑥 ∧ 𝑦 ∈ (𝐹‘𝑧)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))) |
18 | 14, 17 | bitri 275 |
. . . 4
⊢
(∃𝑧 ∈
𝐴 (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))) |
19 | 18 | opabbii 5177 |
. . 3
⊢
{⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐴 (𝑥 ∈ {𝑧} ∧ 𝑦 ∈ (𝐹‘𝑧))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
20 | 8, 9, 19 | 3eqtri 2769 |
. 2
⊢ ∪ 𝑧 ∈ 𝐴 ({𝑧} × (𝐹‘𝑧)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |
21 | 1, 5, 20 | 3eqtri 2769 |
1
⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} |