Step | Hyp | Ref
| Expression |
1 | | vex 3436 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
2 | | eqeq1 2742 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → (𝑧 = 𝐵 ↔ 𝑢 = 𝐵)) |
3 | 2 | rexbidv 3226 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑢 → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵)) |
4 | 1, 3 | elab 3609 |
. . . . . . . . 9
⊢ (𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ↔ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) |
5 | | r19.29 3184 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ∃𝑥 ∈ 𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵)) |
6 | | nfv 1917 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥(Fun 𝑢 ∧ Fun ◡𝑢) |
7 | | nfre1 3239 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵 |
8 | 7 | nfab 2913 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} |
9 | | nfv 1917 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) |
10 | 8, 9 | nfralw 3151 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢) |
11 | 6, 10 | nfan 1902 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
12 | | f1eq1 6665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝐵 → (𝑢:𝐷–1-1→𝑆 ↔ 𝐵:𝐷–1-1→𝑆)) |
13 | 12 | biimparc 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → 𝑢:𝐷–1-1→𝑆) |
14 | | df-f1 6438 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢:𝐷–1-1→𝑆 ↔ (𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢)) |
15 | | ffun 6603 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢:𝐷⟶𝑆 → Fun 𝑢) |
16 | 15 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢:𝐷⟶𝑆 ∧ Fun ◡𝑢) → (Fun 𝑢 ∧ Fun ◡𝑢)) |
17 | 14, 16 | sylbi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑢:𝐷–1-1→𝑆 → (Fun 𝑢 ∧ Fun ◡𝑢)) |
18 | 13, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐵:𝐷–1-1→𝑆 ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢)) |
19 | 18 | adantlr 712 |
. . . . . . . . . . . . 13
⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → (Fun 𝑢 ∧ Fun ◡𝑢)) |
20 | | f1f 6670 |
. . . . . . . . . . . . . 14
⊢ (𝐵:𝐷–1-1→𝑆 → 𝐵:𝐷⟶𝑆) |
21 | | fiun.1 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
22 | 21 | fiunlem 7784 |
. . . . . . . . . . . . . 14
⊢ (((𝐵:𝐷⟶𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
23 | 20, 22 | sylanl1 677 |
. . . . . . . . . . . . 13
⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) |
24 | 19, 23 | jca 512 |
. . . . . . . . . . . 12
⊢ (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
25 | 24 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)))) |
26 | 11, 25 | rexlimi 3248 |
. . . . . . . . . 10
⊢
(∃𝑥 ∈
𝐴 ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
27 | 5, 26 | syl 17 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ ∃𝑥 ∈ 𝐴 𝑢 = 𝐵) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
28 | 4, 27 | sylan2b 594 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) ∧ 𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
29 | 28 | ralrimiva 3103 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑢 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢))) |
30 | | fun11uni 7779 |
. . . . . . 7
⊢
(∀𝑢 ∈
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ((Fun 𝑢 ∧ Fun ◡𝑢) ∧ ∀𝑣 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} (𝑢 ⊆ 𝑣 ∨ 𝑣 ⊆ 𝑢)) → (Fun ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (Fun ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} ∧ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵})) |
32 | 31 | simpld 495 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) |
33 | | fiun.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
34 | 33 | dfiun2 4963 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} |
35 | 34 | funeqi 6455 |
. . . . 5
⊢ (Fun
∪ 𝑥 ∈ 𝐴 𝐵 ↔ Fun ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) |
36 | 32, 35 | sylibr 233 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ∪ 𝑥 ∈ 𝐴 𝐵) |
37 | 1 | eldm2 5810 |
. . . . . . . . 9
⊢ (𝑢 ∈ dom 𝐵 ↔ ∃𝑣〈𝑢, 𝑣〉 ∈ 𝐵) |
38 | | f1dm 6674 |
. . . . . . . . . 10
⊢ (𝐵:𝐷–1-1→𝑆 → dom 𝐵 = 𝐷) |
39 | 38 | eleq2d 2824 |
. . . . . . . . 9
⊢ (𝐵:𝐷–1-1→𝑆 → (𝑢 ∈ dom 𝐵 ↔ 𝑢 ∈ 𝐷)) |
40 | 37, 39 | bitr3id 285 |
. . . . . . . 8
⊢ (𝐵:𝐷–1-1→𝑆 → (∃𝑣〈𝑢, 𝑣〉 ∈ 𝐵 ↔ 𝑢 ∈ 𝐷)) |
41 | 40 | adantr 481 |
. . . . . . 7
⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑣〈𝑢, 𝑣〉 ∈ 𝐵 ↔ 𝑢 ∈ 𝐷)) |
42 | 41 | ralrexbid 3255 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (∃𝑥 ∈ 𝐴 ∃𝑣〈𝑢, 𝑣〉 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷)) |
43 | | eliun 4928 |
. . . . . . . 8
⊢
(〈𝑢, 𝑣〉 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝐵) |
44 | 43 | exbii 1850 |
. . . . . . 7
⊢
(∃𝑣〈𝑢, 𝑣〉 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝐵) |
45 | 1 | eldm2 5810 |
. . . . . . 7
⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑣〈𝑢, 𝑣〉 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) |
46 | | rexcom4 3233 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 ∃𝑣〈𝑢, 𝑣〉 ∈ 𝐵 ↔ ∃𝑣∃𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝐵) |
47 | 44, 45, 46 | 3bitr4i 303 |
. . . . . 6
⊢ (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 ∃𝑣〈𝑢, 𝑣〉 ∈ 𝐵) |
48 | | eliun 4928 |
. . . . . 6
⊢ (𝑢 ∈ ∪ 𝑥 ∈ 𝐴 𝐷 ↔ ∃𝑥 ∈ 𝐴 𝑢 ∈ 𝐷) |
49 | 42, 47, 48 | 3bitr4g 314 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → (𝑢 ∈ dom ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑢 ∈ ∪
𝑥 ∈ 𝐴 𝐷)) |
50 | 49 | eqrdv 2736 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷) |
51 | | df-fn 6436 |
. . . 4
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪
𝑥 ∈ 𝐴 𝐷 ↔ (Fun ∪ 𝑥 ∈ 𝐴 𝐵 ∧ dom ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐷)) |
52 | 36, 50, 51 | sylanbrc 583 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵 Fn ∪
𝑥 ∈ 𝐴 𝐷) |
53 | | rniun 6051 |
. . . 4
⊢ ran
∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 ran 𝐵 |
54 | 20 | frnd 6608 |
. . . . . . 7
⊢ (𝐵:𝐷–1-1→𝑆 → ran 𝐵 ⊆ 𝑆) |
55 | 54 | adantr 481 |
. . . . . 6
⊢ ((𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran 𝐵 ⊆ 𝑆) |
56 | 55 | ralimi 3087 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆) |
57 | | iunss 4975 |
. . . . 5
⊢ (∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆 ↔ ∀𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆) |
58 | 56, 57 | sylibr 233 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 ran 𝐵 ⊆ 𝑆) |
59 | 53, 58 | eqsstrid 3969 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆) |
60 | | df-f 6437 |
. . 3
⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ↔ (∪
𝑥 ∈ 𝐴 𝐵 Fn ∪
𝑥 ∈ 𝐴 𝐷 ∧ ran ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝑆)) |
61 | 52, 59, 60 | sylanbrc 583 |
. 2
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆) |
62 | 31 | simprd 496 |
. . 3
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) |
63 | 34 | cnveqi 5783 |
. . . 4
⊢ ◡∪ 𝑥 ∈ 𝐴 𝐵 = ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵} |
64 | 63 | funeqi 6455 |
. . 3
⊢ (Fun
◡∪
𝑥 ∈ 𝐴 𝐵 ↔ Fun ◡∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) |
65 | 62, 64 | sylibr 233 |
. 2
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → Fun ◡∪ 𝑥 ∈ 𝐴 𝐵) |
66 | | df-f1 6438 |
. 2
⊢ (∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆 ↔ (∪
𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷⟶𝑆 ∧ Fun ◡∪ 𝑥 ∈ 𝐴 𝐵)) |
67 | 61, 65, 66 | sylanbrc 583 |
1
⊢
(∀𝑥 ∈
𝐴 (𝐵:𝐷–1-1→𝑆 ∧ ∀𝑦 ∈ 𝐴 (𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵)) → ∪ 𝑥 ∈ 𝐴 𝐵:∪ 𝑥 ∈ 𝐴 𝐷–1-1→𝑆) |