Step | Hyp | Ref
| Expression |
1 | | fiiuncl.n0 |
. 2
⊢ (𝜑 → 𝐴 ≠ ∅) |
2 | | neeq1 3008 |
. . . 4
⊢ (𝑣 = ∅ → (𝑣 ≠ ∅ ↔ ∅
≠ ∅)) |
3 | | iuneq1 4946 |
. . . . 5
⊢ (𝑣 = ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵) |
4 | 3 | eleq1d 2825 |
. . . 4
⊢ (𝑣 = ∅ → (∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪
𝑥 ∈ ∅ 𝐵 ∈ 𝐷)) |
5 | 2, 4 | imbi12d 345 |
. . 3
⊢ (𝑣 = ∅ → ((𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷) ↔ (∅ ≠ ∅ →
∪ 𝑥 ∈ ∅ 𝐵 ∈ 𝐷))) |
6 | | neeq1 3008 |
. . . 4
⊢ (𝑣 = 𝑤 → (𝑣 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
7 | | iuneq1 4946 |
. . . . 5
⊢ (𝑣 = 𝑤 → ∪
𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ 𝑤 𝐵) |
8 | 7 | eleq1d 2825 |
. . . 4
⊢ (𝑣 = 𝑤 → (∪
𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) |
9 | 6, 8 | imbi12d 345 |
. . 3
⊢ (𝑣 = 𝑤 → ((𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷) ↔ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷))) |
10 | | neeq1 3008 |
. . . 4
⊢ (𝑣 = (𝑤 ∪ {𝑢}) → (𝑣 ≠ ∅ ↔ (𝑤 ∪ {𝑢}) ≠ ∅)) |
11 | | iuneq1 4946 |
. . . . 5
⊢ (𝑣 = (𝑤 ∪ {𝑢}) → ∪
𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵) |
12 | 11 | eleq1d 2825 |
. . . 4
⊢ (𝑣 = (𝑤 ∪ {𝑢}) → (∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪
𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 ∈ 𝐷)) |
13 | 10, 12 | imbi12d 345 |
. . 3
⊢ (𝑣 = (𝑤 ∪ {𝑢}) → ((𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷) ↔ ((𝑤 ∪ {𝑢}) ≠ ∅ → ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 ∈ 𝐷))) |
14 | | neeq1 3008 |
. . . 4
⊢ (𝑣 = 𝐴 → (𝑣 ≠ ∅ ↔ 𝐴 ≠ ∅)) |
15 | | iuneq1 4946 |
. . . . 5
⊢ (𝑣 = 𝐴 → ∪
𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) |
16 | 15 | eleq1d 2825 |
. . . 4
⊢ (𝑣 = 𝐴 → (∪
𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝐷)) |
17 | 14, 16 | imbi12d 345 |
. . 3
⊢ (𝑣 = 𝐴 → ((𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷) ↔ (𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷))) |
18 | | neirr 2954 |
. . . . 5
⊢ ¬
∅ ≠ ∅ |
19 | 18 | pm2.21i 119 |
. . . 4
⊢ (∅
≠ ∅ → ∪ 𝑥 ∈ ∅ 𝐵 ∈ 𝐷) |
20 | 19 | a1i 11 |
. . 3
⊢ (𝜑 → (∅ ≠ ∅
→ ∪ 𝑥 ∈ ∅ 𝐵 ∈ 𝐷)) |
21 | | iunxun 5028 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 = (∪
𝑥 ∈ 𝑤 𝐵 ∪ ∪
𝑥 ∈ {𝑢}𝐵) |
22 | | nfcsb1v 3862 |
. . . . . . . . . 10
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 |
23 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
24 | | csbeq1a 3851 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → 𝐵 = ⦋𝑢 / 𝑥⦌𝐵) |
25 | 22, 23, 24 | iunxsnf 42582 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ {𝑢}𝐵 = ⦋𝑢 / 𝑥⦌𝐵 |
26 | 25 | uneq2i 4099 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ∪
𝑥 ∈ {𝑢}𝐵) = (∪
𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) |
27 | 21, 26 | eqtri 2768 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 = (∪
𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) |
28 | | iuneq1 4946 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵) |
29 | | 0iun 4997 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅ |
30 | 29 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = ∅ → ∪ 𝑥 ∈ ∅ 𝐵 = ∅) |
31 | 28, 30 | eqtrd 2780 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∅) |
32 | 31 | uneq1d 4101 |
. . . . . . . . . . . 12
⊢ (𝑤 = ∅ → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) = (∅ ∪ ⦋𝑢 / 𝑥⦌𝐵)) |
33 | | 0un 4332 |
. . . . . . . . . . . . . 14
⊢ (∅
∪ ⦋𝑢 /
𝑥⦌𝐵) = ⦋𝑢 / 𝑥⦌𝐵 |
34 | | unidm 4091 |
. . . . . . . . . . . . . 14
⊢
(⦋𝑢 /
𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) = ⦋𝑢 / 𝑥⦌𝐵 |
35 | 33, 34 | eqtr4i 2771 |
. . . . . . . . . . . . 13
⊢ (∅
∪ ⦋𝑢 /
𝑥⦌𝐵) = (⦋𝑢 / 𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) |
36 | 35 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑤 = ∅ → (∅ ∪
⦋𝑢 / 𝑥⦌𝐵) = (⦋𝑢 / 𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵)) |
37 | 32, 36 | eqtrd 2780 |
. . . . . . . . . . 11
⊢ (𝑤 = ∅ → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) = (⦋𝑢 / 𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵)) |
38 | 37 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ 𝑤 = ∅) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) = (⦋𝑢 / 𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵)) |
39 | | simpl 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) → 𝜑) |
40 | | eldifi 4066 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ (𝐴 ∖ 𝑤) → 𝑢 ∈ 𝐴) |
41 | 40 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) → 𝑢 ∈ 𝐴) |
42 | | fiiuncl.xph |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥𝜑 |
43 | | nfv 1921 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑢 ∈ 𝐴 |
44 | 42, 43 | nfan 1906 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝜑 ∧ 𝑢 ∈ 𝐴) |
45 | | nfcv 2909 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥𝐷 |
46 | 22, 45 | nfel 2923 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷 |
47 | 44, 46 | nfim 1903 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷) |
48 | | eleq1 2828 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑢 → (𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴)) |
49 | 48 | anbi2d 629 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → ((𝜑 ∧ 𝑥 ∈ 𝐴) ↔ (𝜑 ∧ 𝑢 ∈ 𝐴))) |
50 | 24 | eleq1d 2825 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → (𝐵 ∈ 𝐷 ↔ ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷)) |
51 | 49, 50 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → (((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷) ↔ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷))) |
52 | | fiiuncl.b |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝐷) |
53 | 47, 51, 52 | chvarfv 2237 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷) |
54 | 34, 53 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴) → (⦋𝑢 / 𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
55 | 39, 41, 54 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) → (⦋𝑢 / 𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
56 | 55 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ 𝑤 = ∅) → (⦋𝑢 / 𝑥⦌𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
57 | 38, 56 | eqeltrd 2841 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ 𝑤 = ∅) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
58 | 57 | adantlr 712 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) ∧ 𝑤 = ∅) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
59 | | simplll 772 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) ∧ ¬ 𝑤 = ∅) → 𝜑) |
60 | 40 | ad3antlr 728 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) ∧ ¬ 𝑤 = ∅) → 𝑢 ∈ 𝐴) |
61 | | neqne 2953 |
. . . . . . . . . . . 12
⊢ (¬
𝑤 = ∅ → 𝑤 ≠ ∅) |
62 | 61 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) ∧ ¬ 𝑤 = ∅) → 𝑤 ≠ ∅) |
63 | | simpl 483 |
. . . . . . . . . . 11
⊢ (((𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) ∧ ¬ 𝑤 = ∅) → (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) |
64 | 62, 63 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) ∧ ¬ 𝑤 = ∅) → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) |
65 | 64 | adantll 711 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) ∧ ¬ 𝑤 = ∅) → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) |
66 | 53 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) → ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷) |
67 | | simp3 1137 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) → ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) |
68 | | simp1 1135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) → 𝜑) |
69 | 68, 67, 66 | 3jca 1127 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) → (𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷)) |
70 | | eleq1 2828 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ⦋𝑢 / 𝑥⦌𝐵 → (𝑧 ∈ 𝐷 ↔ ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷)) |
71 | 70 | 3anbi3d 1441 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ⦋𝑢 / 𝑥⦌𝐵 → ((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) ↔ (𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷))) |
72 | | uneq2 4096 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ⦋𝑢 / 𝑥⦌𝐵 → (∪
𝑥 ∈ 𝑤 𝐵 ∪ 𝑧) = (∪
𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵)) |
73 | 72 | eleq1d 2825 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ⦋𝑢 / 𝑥⦌𝐵 → ((∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧) ∈ 𝐷 ↔ (∪
𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷)) |
74 | 71, 73 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑧 = ⦋𝑢 / 𝑥⦌𝐵 → (((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧) ∈ 𝐷) ↔ ((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷))) |
75 | 74 | imbi2d 341 |
. . . . . . . . . . 11
⊢ (𝑧 = ⦋𝑢 / 𝑥⦌𝐵 → ((∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧) ∈ 𝐷)) ↔ (∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷)))) |
76 | | eleq1 2828 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → (𝑦 ∈ 𝐷 ↔ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) |
77 | 76 | 3anbi2d 1440 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → ((𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) ↔ (𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷))) |
78 | | uneq1 4095 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → (𝑦 ∪ 𝑧) = (∪
𝑥 ∈ 𝑤 𝐵 ∪ 𝑧)) |
79 | 78 | eleq1d 2825 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → ((𝑦 ∪ 𝑧) ∈ 𝐷 ↔ (∪
𝑥 ∈ 𝑤 𝐵 ∪ 𝑧) ∈ 𝐷)) |
80 | 77, 79 | imbi12d 345 |
. . . . . . . . . . . 12
⊢ (𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → (((𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝑦 ∪ 𝑧) ∈ 𝐷) ↔ ((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧) ∈ 𝐷))) |
81 | | fiiuncl.un |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (𝑦 ∪ 𝑧) ∈ 𝐷) |
82 | 80, 81 | vtoclg 3504 |
. . . . . . . . . . 11
⊢ (∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧) ∈ 𝐷)) |
83 | 75, 82 | vtoclg 3504 |
. . . . . . . . . 10
⊢
(⦋𝑢 /
𝑥⦌𝐵 ∈ 𝐷 → (∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ((𝜑 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋𝑢 / 𝑥⦌𝐵 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷))) |
84 | 66, 67, 69, 83 | syl3c 66 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪
𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
85 | 59, 60, 65, 84 | syl3anc 1370 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) ∧ ¬ 𝑤 = ∅) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
86 | 58, 85 | pm2.61dan 810 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) → (∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋𝑢 / 𝑥⦌𝐵) ∈ 𝐷) |
87 | 27, 86 | eqeltrid 2845 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) → ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 ∈ 𝐷) |
88 | 87 | a1d 25 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) ∧ (𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷)) → ((𝑤 ∪ {𝑢}) ≠ ∅ → ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 ∈ 𝐷)) |
89 | 88 | ex 413 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤)) → ((𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) → ((𝑤 ∪ {𝑢}) ≠ ∅ → ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 ∈ 𝐷))) |
90 | 89 | adantrl 713 |
. . 3
⊢ ((𝜑 ∧ (𝑤 ⊆ 𝐴 ∧ 𝑢 ∈ (𝐴 ∖ 𝑤))) → ((𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷) → ((𝑤 ∪ {𝑢}) ≠ ∅ → ∪ 𝑥 ∈ (𝑤 ∪ {𝑢})𝐵 ∈ 𝐷))) |
91 | | fiiuncl.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
92 | 5, 9, 13, 17, 20, 90, 91 | findcard2d 8931 |
. 2
⊢ (𝜑 → (𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷)) |
93 | 1, 92 | mpd 15 |
1
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷) |