Step | Hyp | Ref
| Expression |
1 | | vex 3470 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
2 | | eqeq1 2728 |
. . . . . . . . 9
⊢ (𝑧 = 𝑢 → (𝑧 = 𝐵 ↔ 𝑢 = 𝐵)) |
3 | 2 | rexbidv 3170 |
. . . . . . . 8
⊢ (𝑧 = 𝑢 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵)) |
4 | 1, 3 | elab 3660 |
. . . . . . 7
⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) |
5 | | r19.29 3106 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ∃𝑥 ∈ 𝐴 ((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵)) |
6 | | nfv 1909 |
. . . . . . . . . 10
⊢
Ⅎ𝑥Fun 𝑢 |
7 | | nfre1 3274 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵 |
8 | 7 | nfab 2901 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} |
9 | | nfv 1909 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) |
10 | 8, 9 | nfralw 3300 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) |
11 | 6, 10 | nfan 1894 |
. . . . . . . . 9
⊢
Ⅎ𝑥(Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
12 | | ffun 6710 |
. . . . . . . . . . . . 13
⊢ (𝐵:𝐷⟶𝑆 → Fun 𝐵) |
13 | | funeq 6558 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝐵 → (Fun 𝑢 ↔ Fun 𝐵)) |
14 | | bianir 1055 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐵 ∧ (Fun 𝑢 ↔ Fun 𝐵)) → Fun 𝑢) |
15 | 12, 13, 14 | syl2an 595 |
. . . . . . . . . . . 12
⊢ ((𝐵:𝐷⟶𝑆 ∧ 𝑢 = 𝐵) → Fun 𝑢) |
16 | 15 | adantlr 712 |
. . . . . . . . . . 11
⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → Fun 𝑢) |
17 | | fiun.1 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
18 | 17 | fiunlem 7921 |
. . . . . . . . . . 11
⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
19 | 16, 18 | jca 511 |
. . . . . . . . . 10
⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
21 | 11, 20 | rexlimi 3248 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
22 | 5, 21 | syl 17 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
23 | 4, 22 | sylan2b 593 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
24 | 23 | ralrimiva 3138 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
25 | | fununi 6613 |
. . . . 5
⊢
(∀𝑢 ∈
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (Fun 𝑢 ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → Fun ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) |
26 | 24, 25 | syl 17 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) |
27 | | fiun.2 |
. . . . . 6
⊢ 𝐵 ∈ V |
28 | 27 | dfiun2 5026 |
. . . . 5
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} |
29 | 28 | funeqi 6559 |
. . . 4
⊢ (Fun
∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) |
30 | 26, 29 | sylibr 233 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ 𝑥 ∈ 𝐴 𝐵) |
31 | 1 | eldm2 5891 |
. . . . . . . 8
⊢ (𝑢 ∈ dom 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵) |
32 | | fdm 6716 |
. . . . . . . . 9
⊢ (𝐵:𝐷⟶𝑆 → dom 𝐵 = 𝐷) |
33 | 32 | eleq2d 2811 |
. . . . . . . 8
⊢ (𝐵:𝐷⟶𝑆 → (𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷)) |
34 | 31, 33 | bitr3id 285 |
. . . . . . 7
⊢ (𝐵:𝐷⟶𝑆 → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷)) |
35 | 34 | adantr 480 |
. . . . . 6
⊢ ((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ 𝑢 ∈ 𝐷)) |
36 | 35 | ralrexbid 3098 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷)) |
37 | | eliun 4991 |
. . . . . . 7
⊢
(⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵) |
38 | 37 | exbii 1842 |
. . . . . 6
⊢
(∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵) |
39 | 1 | eldm2 5891 |
. . . . . 6
⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣⟨𝑢, 𝑣⟩ ∈ ∪ 𝑥 ∈ 𝐴 𝐵) |
40 | | rexcom4 3277 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 ⟨𝑢, 𝑣⟩ ∈ 𝐵) |
41 | 38, 39, 40 | 3bitr4i 303 |
. . . . 5
⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑣⟨𝑢, 𝑣⟩ ∈ 𝐵) |
42 | | eliun 4991 |
. . . . 5
⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷) |
43 | 36, 41, 42 | 3bitr4g 314 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪
𝑥 ∈ 𝐴 𝐷)) |
44 | 43 | eqrdv 2722 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷) |
45 | | df-fn 6536 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪
𝑥 ∈ 𝐴 𝐷 ↔ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷)) |
46 | 30, 44, 45 | sylanbrc 582 |
. 2
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪
𝑥 ∈ 𝐴 𝐷) |
47 | | rniun 6137 |
. . 3
⊢ ran
∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵 |
48 | | frn 6714 |
. . . . . 6
⊢ (𝐵:𝐷⟶𝑆 → ran 𝐵 ⊆ 𝑆) |
49 | 48 | adantr 480 |
. . . . 5
⊢ ((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran 𝐵 ⊆ 𝑆) |
50 | 49 | ralimi 3075 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆) |
51 | | iunss 5038 |
. . . 4
⊢ (∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆) |
52 | 50, 51 | sylibr 233 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆) |
53 | 47, 52 | eqsstrid 4022 |
. 2
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆) |
54 | | df-f 6537 |
. 2
⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ↔ (∪
𝑥 ∈ 𝐴 𝐵 Fn ∪
𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆)) |
55 | 46, 53, 54 | sylanbrc 582 |
1
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆) |