Step | Hyp | Ref
| Expression |
1 | | dffun7 4871 |
. . . . . . . . . 10
⊢ (Fun
A ↔ (Rel A ∧ ∀x ∈ dom A∃*y xAy)) |
2 | 1 | simprbi 260 |
. . . . . . . . 9
⊢ (Fun
A → ∀x ∈ dom A∃*y xAy) |
3 | 2 | 3ad2ant1 924 |
. . . . . . . 8
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∀x ∈ dom A∃*y xAy) |
4 | | ssralv 2998 |
. . . . . . . . 9
⊢ (B ⊆ dom A
→ (∀x ∈ dom A∃*y xAy → ∀x ∈ B ∃*y xAy)) |
5 | 4 | 3ad2ant3 926 |
. . . . . . . 8
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → (∀x ∈ dom A∃*y xAy → ∀x ∈ B ∃*y xAy)) |
6 | 3, 5 | mpd 13 |
. . . . . . 7
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∀x ∈ B ∃*y xAy) |
7 | 6 | alrimiv 1751 |
. . . . . 6
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∀z∀x ∈ B ∃*y xAy) |
8 | | sseq1 2960 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = B → (𝑏 ⊆ dom A ↔ B
⊆ dom A)) |
9 | 8 | biimpar 281 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 = B ∧ B ⊆ dom A)
→ 𝑏 ⊆ dom A) |
10 | 9 | 3adant1 921 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
A ∧ 𝑏 = B ∧ B ⊆ dom A)
→ 𝑏 ⊆ dom A) |
11 | | simp1 903 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
A ∧ 𝑏 = B ∧ B ⊆ dom A)
→ Fun A) |
12 | 10, 11 | jca 290 |
. . . . . . . . . . . . . 14
⊢ ((Fun
A ∧ 𝑏 = B ∧ B ⊆ dom A)
→ (𝑏 ⊆ dom A ∧ Fun A)) |
13 | | dffun8 4872 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
A ↔ (Rel A ∧ ∀x ∈ dom A∃!y xAy)) |
14 | 13 | simprbi 260 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
A → ∀x ∈ dom A∃!y xAy) |
15 | 14 | adantl 262 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ⊆ dom A ∧ Fun A) → ∀x ∈ dom A∃!y xAy) |
16 | | ssel 2933 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ⊆ dom A → (x
∈ 𝑏 → x
∈ dom A)) |
17 | 16 | adantr 261 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ⊆ dom A ∧ Fun A) → (x
∈ 𝑏 → x
∈ dom A)) |
18 | | rsp 2363 |
. . . . . . . . . . . . . . . 16
⊢ (∀x ∈ dom A∃!y xAy → (x
∈ dom A
→ ∃!y xAy)) |
19 | 15, 17, 18 | sylsyld 52 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ⊆ dom A ∧ Fun A) → (x
∈ 𝑏 → ∃!y xAy)) |
20 | 19 | ralrimiv 2385 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ⊆ dom A ∧ Fun A) → ∀x ∈ 𝑏 ∃!y xAy) |
21 | | zfrep6 3865 |
. . . . . . . . . . . . . 14
⊢ (∀x ∈ 𝑏 ∃!y xAy → ∃z∀x ∈ 𝑏 ∃y ∈ z xAy) |
22 | 12, 20, 21 | 3syl 17 |
. . . . . . . . . . . . 13
⊢ ((Fun
A ∧ 𝑏 = B ∧ B ⊆ dom A)
→ ∃z∀x ∈ 𝑏 ∃y ∈ z xAy) |
23 | | raleq 2499 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = B → (∀x ∈ 𝑏 ∃y ∈ z xAy ↔ ∀x ∈ B ∃y ∈ z xAy)) |
24 | 23 | exbidv 1703 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = B → (∃z∀x ∈ 𝑏 ∃y ∈ z xAy ↔ ∃z∀x ∈ B ∃y ∈ z xAy)) |
25 | 24 | 3ad2ant2 925 |
. . . . . . . . . . . . 13
⊢ ((Fun
A ∧ 𝑏 = B ∧ B ⊆ dom A)
→ (∃z∀x ∈ 𝑏 ∃y ∈ z xAy ↔ ∃z∀x ∈ B ∃y ∈ z xAy)) |
26 | 22, 25 | mpbid 135 |
. . . . . . . . . . . 12
⊢ ((Fun
A ∧ 𝑏 = B ∧ B ⊆ dom A)
→ ∃z∀x ∈ B ∃y ∈ z xAy) |
27 | 26 | 3com12 1107 |
. . . . . . . . . . 11
⊢ ((𝑏 = B ∧ Fun A ∧ B ⊆ dom A)
→ ∃z∀x ∈ B ∃y ∈ z xAy) |
28 | 27 | 3expib 1106 |
. . . . . . . . . 10
⊢ (𝑏 = B → ((Fun A
∧ B
⊆ dom A) → ∃z∀x ∈ B ∃y ∈ z xAy)) |
29 | 28 | vtocleg 2618 |
. . . . . . . . 9
⊢ (B ∈ 𝐶 → ((Fun A ∧ B ⊆ dom A)
→ ∃z∀x ∈ B ∃y ∈ z xAy)) |
30 | 29 | 3impib 1101 |
. . . . . . . 8
⊢
((B ∈ 𝐶 ∧ Fun
A ∧
B ⊆ dom A) → ∃z∀x ∈ B ∃y ∈ z xAy) |
31 | 30 | 3com12 1107 |
. . . . . . 7
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∃z∀x ∈ B ∃y ∈ z xAy) |
32 | | df-rex 2306 |
. . . . . . . . . 10
⊢ (∃y ∈ z xAy ↔ ∃y(y ∈ z ∧ xAy)) |
33 | | exancom 1496 |
. . . . . . . . . 10
⊢ (∃y(y ∈ z ∧ xAy) ↔ ∃y(xAy ∧ y ∈ z)) |
34 | 32, 33 | bitri 173 |
. . . . . . . . 9
⊢ (∃y ∈ z xAy ↔ ∃y(xAy ∧ y ∈ z)) |
35 | 34 | ralbii 2324 |
. . . . . . . 8
⊢ (∀x ∈ B ∃y ∈ z xAy ↔ ∀x ∈ B ∃y(xAy ∧ y ∈ z)) |
36 | 35 | exbii 1493 |
. . . . . . 7
⊢ (∃z∀x ∈ B ∃y ∈ z xAy ↔ ∃z∀x ∈ B ∃y(xAy ∧ y ∈ z)) |
37 | 31, 36 | sylib 127 |
. . . . . 6
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∃z∀x ∈ B ∃y(xAy ∧ y ∈ z)) |
38 | | 19.29 1508 |
. . . . . . 7
⊢ ((∀z∀x ∈ B ∃*y xAy ∧ ∃z∀x ∈ B ∃y(xAy ∧ y ∈ z)) → ∃z(∀x ∈ B ∃*y xAy ∧ ∀x ∈ B ∃y(xAy ∧ y ∈ z))) |
39 | | nfcv 2175 |
. . . . . . . . . . 11
⊢
ℲyB |
40 | | nfmo1 1909 |
. . . . . . . . . . 11
⊢
Ⅎy∃*y xAy |
41 | 39, 40 | nfralxy 2354 |
. . . . . . . . . 10
⊢
Ⅎy∀x ∈ B ∃*y xAy |
42 | | nfe1 1382 |
. . . . . . . . . . 11
⊢
Ⅎy∃y(xAy ∧ y ∈ z) |
43 | 39, 42 | nfralxy 2354 |
. . . . . . . . . 10
⊢
Ⅎy∀x ∈ B ∃y(xAy ∧ y ∈ z) |
44 | 41, 43 | nfan 1454 |
. . . . . . . . 9
⊢
Ⅎy(∀x ∈ B ∃*y xAy ∧ ∀x ∈ B ∃y(xAy ∧ y ∈ z)) |
45 | | r19.26 2435 |
. . . . . . . . . 10
⊢ (∀x ∈ B (∃*y xAy ∧ ∃y(xAy ∧ y ∈ z)) ↔ (∀x ∈ B ∃*y xAy ∧ ∀x ∈ B ∃y(xAy ∧ y ∈ z))) |
46 | | mopick 1975 |
. . . . . . . . . . 11
⊢ ((∃*y xAy ∧ ∃y(xAy ∧ y ∈ z)) → (xAy → y ∈ z)) |
47 | 46 | ralimi 2378 |
. . . . . . . . . 10
⊢ (∀x ∈ B (∃*y xAy ∧ ∃y(xAy ∧ y ∈ z)) → ∀x ∈ B (xAy → y ∈ z)) |
48 | 45, 47 | sylbir 125 |
. . . . . . . . 9
⊢ ((∀x ∈ B ∃*y xAy ∧ ∀x ∈ B ∃y(xAy ∧ y ∈ z)) → ∀x ∈ B (xAy → y ∈ z)) |
49 | 44, 48 | alrimi 1412 |
. . . . . . . 8
⊢ ((∀x ∈ B ∃*y xAy ∧ ∀x ∈ B ∃y(xAy ∧ y ∈ z)) → ∀y∀x ∈ B (xAy → y ∈ z)) |
50 | 49 | eximi 1488 |
. . . . . . 7
⊢ (∃z(∀x ∈ B ∃*y xAy ∧ ∀x ∈ B ∃y(xAy ∧ y ∈ z)) → ∃z∀y∀x ∈ B (xAy → y ∈ z)) |
51 | 38, 50 | syl 14 |
. . . . . 6
⊢ ((∀z∀x ∈ B ∃*y xAy ∧ ∃z∀x ∈ B ∃y(xAy ∧ y ∈ z)) → ∃z∀y∀x ∈ B (xAy → y ∈ z)) |
52 | 7, 37, 51 | syl2anc 391 |
. . . . 5
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∃z∀y∀x ∈ B (xAy → y ∈ z)) |
53 | | r19.23v 2419 |
. . . . . . 7
⊢ (∀x ∈ B (xAy → y ∈ z) ↔
(∃x
∈ B
xAy →
y ∈
z)) |
54 | 53 | albii 1356 |
. . . . . 6
⊢ (∀y∀x ∈ B (xAy → y ∈ z) ↔
∀y(∃x ∈ B xAy →
y ∈
z)) |
55 | 54 | exbii 1493 |
. . . . 5
⊢ (∃z∀y∀x ∈ B (xAy → y ∈ z) ↔
∃z∀y(∃x ∈ B xAy → y ∈ z)) |
56 | 52, 55 | sylib 127 |
. . . 4
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∃z∀y(∃x ∈ B xAy → y ∈ z)) |
57 | | abss 3003 |
. . . . 5
⊢
({y ∣ ∃x ∈ B xAy} ⊆ z
↔ ∀y(∃x ∈ B xAy →
y ∈
z)) |
58 | 57 | exbii 1493 |
. . . 4
⊢ (∃z{y ∣ ∃x ∈ B xAy} ⊆ z
↔ ∃z∀y(∃x ∈ B xAy →
y ∈
z)) |
59 | 56, 58 | sylibr 137 |
. . 3
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∃z{y ∣ ∃x ∈ B xAy} ⊆ z) |
60 | | dfima2 4613 |
. . . . 5
⊢ (A “ B) =
{y ∣ ∃x ∈ B xAy} |
61 | 60 | sseq1i 2963 |
. . . 4
⊢
((A “ B) ⊆ z
↔ {y ∣ ∃x ∈ B xAy} ⊆ z) |
62 | 61 | exbii 1493 |
. . 3
⊢ (∃z(A “ B)
⊆ z ↔ ∃z{y ∣ ∃x ∈ B xAy} ⊆ z) |
63 | 59, 62 | sylibr 137 |
. 2
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → ∃z(A “ B)
⊆ z) |
64 | | vex 2554 |
. . . 4
⊢ z ∈
V |
65 | 64 | ssex 3885 |
. . 3
⊢
((A “ B) ⊆ z
→ (A “ B) ∈
V) |
66 | 65 | exlimiv 1486 |
. 2
⊢ (∃z(A “ B)
⊆ z → (A “ B)
∈ V) |
67 | 63, 66 | syl 14 |
1
⊢ ((Fun
A ∧
B ∈ 𝐶 ∧ B ⊆ dom
A) → (A “ B)
∈ V) |