Step | Hyp | Ref
| Expression |
1 | | iunmapsn.x |
. . 3
⊢
Ⅎ𝑥𝜑 |
2 | | iunmapsn.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | iunmapsn.b |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
4 | 1, 2, 3 | iunmapss 42714 |
. 2
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶}) ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) |
5 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) → 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) |
6 | 3 | ex 413 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑊)) |
7 | 1, 6 | ralrimi 3140 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
8 | | iunexg 7796 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪
𝑥 ∈ 𝐴 𝐵 ∈ V) |
9 | 2, 7, 8 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) |
10 | | iunmapsn.c |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝑍) |
11 | 9, 10 | mapsnd 8662 |
. . . . . . 7
⊢ (𝜑 → (∪ 𝑥 ∈ 𝐴 𝐵 ↑m {𝐶}) = {𝑓 ∣ ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉}}) |
12 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) → (∪ 𝑥 ∈ 𝐴 𝐵 ↑m {𝐶}) = {𝑓 ∣ ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉}}) |
13 | 5, 12 | eleqtrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) → 𝑓 ∈ {𝑓 ∣ ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉}}) |
14 | | abid 2719 |
. . . . 5
⊢ (𝑓 ∈ {𝑓 ∣ ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉}} ↔ ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉}) |
15 | 13, 14 | sylib 217 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) → ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉}) |
16 | | eliun 4929 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
17 | 16 | biimpi 215 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
18 | 17 | 3ad2ant2 1133 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = {〈𝐶, 𝑦〉}) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
19 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑦 |
20 | | nfiu1 4959 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
21 | 19, 20 | nfel 2921 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 |
22 | | nfv 1917 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑓 = {〈𝐶, 𝑦〉} |
23 | 1, 21, 22 | nf3an 1904 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = {〈𝐶, 𝑦〉}) |
24 | | rspe 3235 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑓 = {〈𝐶, 𝑦〉}) → ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}) |
25 | 24 | ancoms 459 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 = {〈𝐶, 𝑦〉} ∧ 𝑦 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}) |
26 | | abid 2719 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}} ↔ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}) |
27 | 25, 26 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = {〈𝐶, 𝑦〉} ∧ 𝑦 ∈ 𝐵) → 𝑓 ∈ {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}}) |
28 | 27 | adantll 711 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 = {〈𝐶, 𝑦〉}) ∧ 𝑦 ∈ 𝐵) → 𝑓 ∈ {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}}) |
29 | 28 | 3adant2 1130 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 = {〈𝐶, 𝑦〉}) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑓 ∈ {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}}) |
30 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑍) |
31 | 3, 30 | mapsnd 8662 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐵 ↑m {𝐶}) = {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}}) |
32 | 31 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}} = (𝐵 ↑m {𝐶})) |
33 | 32 | 3adant3 1131 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}} = (𝐵 ↑m {𝐶})) |
34 | 33 | 3adant1r 1176 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 = {〈𝐶, 𝑦〉}) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {𝑓 ∣ ∃𝑦 ∈ 𝐵 𝑓 = {〈𝐶, 𝑦〉}} = (𝐵 ↑m {𝐶})) |
35 | 29, 34 | eleqtrd 2841 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 = {〈𝐶, 𝑦〉}) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑓 ∈ (𝐵 ↑m {𝐶})) |
36 | 35 | 3exp 1118 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 = {〈𝐶, 𝑦〉}) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑓 ∈ (𝐵 ↑m {𝐶})))) |
37 | 36 | 3adant2 1130 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = {〈𝐶, 𝑦〉}) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝑓 ∈ (𝐵 ↑m {𝐶})))) |
38 | 23, 37 | reximdai 3242 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = {〈𝐶, 𝑦〉}) → (∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑓 ∈ (𝐵 ↑m {𝐶}))) |
39 | 18, 38 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ∧ 𝑓 = {〈𝐶, 𝑦〉}) → ∃𝑥 ∈ 𝐴 𝑓 ∈ (𝐵 ↑m {𝐶})) |
40 | 39 | 3exp 1118 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → (𝑓 = {〈𝐶, 𝑦〉} → ∃𝑥 ∈ 𝐴 𝑓 ∈ (𝐵 ↑m {𝐶})))) |
41 | 40 | rexlimdv 3210 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉} → ∃𝑥 ∈ 𝐴 𝑓 ∈ (𝐵 ↑m {𝐶}))) |
42 | 41 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) → (∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑓 = {〈𝐶, 𝑦〉} → ∃𝑥 ∈ 𝐴 𝑓 ∈ (𝐵 ↑m {𝐶}))) |
43 | 15, 42 | mpd 15 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) → ∃𝑥 ∈ 𝐴 𝑓 ∈ (𝐵 ↑m {𝐶})) |
44 | | eliun 4929 |
. . 3
⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶}) ↔ ∃𝑥 ∈ 𝐴 𝑓 ∈ (𝐵 ↑m {𝐶})) |
45 | 43, 44 | sylibr 233 |
. 2
⊢ ((𝜑 ∧ 𝑓 ∈ (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) → 𝑓 ∈ ∪
𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶})) |
46 | 4, 45 | eqelssd 3942 |
1
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 (𝐵 ↑m {𝐶}) = (∪
𝑥 ∈ 𝐴 𝐵 ↑m {𝐶})) |