Step |
Hyp |
Ref |
Expression |
1 |
|
fiiuncl.xph |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
fiiuncl.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐷 ) |
3 |
|
fiiuncl.un |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( 𝑦 ∪ 𝑧 ) ∈ 𝐷 ) |
4 |
|
fiiuncl.a |
⊢ ( 𝜑 → 𝐴 ∈ Fin ) |
5 |
|
fiiuncl.n0 |
⊢ ( 𝜑 → 𝐴 ≠ ∅ ) |
6 |
|
neeq1 |
⊢ ( 𝑣 = ∅ → ( 𝑣 ≠ ∅ ↔ ∅ ≠ ∅ ) ) |
7 |
|
iuneq1 |
⊢ ( 𝑣 = ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 ) |
8 |
7
|
eleq1d |
⊢ ( 𝑣 = ∅ → ( ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪ 𝑥 ∈ ∅ 𝐵 ∈ 𝐷 ) ) |
9 |
6 8
|
imbi12d |
⊢ ( 𝑣 = ∅ → ( ( 𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ) ↔ ( ∅ ≠ ∅ → ∪ 𝑥 ∈ ∅ 𝐵 ∈ 𝐷 ) ) ) |
10 |
|
neeq1 |
⊢ ( 𝑣 = 𝑤 → ( 𝑣 ≠ ∅ ↔ 𝑤 ≠ ∅ ) ) |
11 |
|
iuneq1 |
⊢ ( 𝑣 = 𝑤 → ∪ 𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ 𝑤 𝐵 ) |
12 |
11
|
eleq1d |
⊢ ( 𝑣 = 𝑤 → ( ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) |
13 |
10 12
|
imbi12d |
⊢ ( 𝑣 = 𝑤 → ( ( 𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ) ↔ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) ) |
14 |
|
neeq1 |
⊢ ( 𝑣 = ( 𝑤 ∪ { 𝑢 } ) → ( 𝑣 ≠ ∅ ↔ ( 𝑤 ∪ { 𝑢 } ) ≠ ∅ ) ) |
15 |
|
iuneq1 |
⊢ ( 𝑣 = ( 𝑤 ∪ { 𝑢 } ) → ∪ 𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 ) |
16 |
15
|
eleq1d |
⊢ ( 𝑣 = ( 𝑤 ∪ { 𝑢 } ) → ( ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 ∈ 𝐷 ) ) |
17 |
14 16
|
imbi12d |
⊢ ( 𝑣 = ( 𝑤 ∪ { 𝑢 } ) → ( ( 𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ) ↔ ( ( 𝑤 ∪ { 𝑢 } ) ≠ ∅ → ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 ∈ 𝐷 ) ) ) |
18 |
|
neeq1 |
⊢ ( 𝑣 = 𝐴 → ( 𝑣 ≠ ∅ ↔ 𝐴 ≠ ∅ ) ) |
19 |
|
iuneq1 |
⊢ ( 𝑣 = 𝐴 → ∪ 𝑥 ∈ 𝑣 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 ) |
20 |
19
|
eleq1d |
⊢ ( 𝑣 = 𝐴 → ( ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ↔ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 ) ) |
21 |
18 20
|
imbi12d |
⊢ ( 𝑣 = 𝐴 → ( ( 𝑣 ≠ ∅ → ∪ 𝑥 ∈ 𝑣 𝐵 ∈ 𝐷 ) ↔ ( 𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 ) ) ) |
22 |
|
neirr |
⊢ ¬ ∅ ≠ ∅ |
23 |
22
|
pm2.21i |
⊢ ( ∅ ≠ ∅ → ∪ 𝑥 ∈ ∅ 𝐵 ∈ 𝐷 ) |
24 |
23
|
a1i |
⊢ ( 𝜑 → ( ∅ ≠ ∅ → ∪ 𝑥 ∈ ∅ 𝐵 ∈ 𝐷 ) ) |
25 |
|
iunxun |
⊢ ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ∪ 𝑥 ∈ { 𝑢 } 𝐵 ) |
26 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ 𝐵 |
27 |
|
vex |
⊢ 𝑢 ∈ V |
28 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑢 → 𝐵 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) |
29 |
26 27 28
|
iunxsnf |
⊢ ∪ 𝑥 ∈ { 𝑢 } 𝐵 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 |
30 |
29
|
uneq2i |
⊢ ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ∪ 𝑥 ∈ { 𝑢 } 𝐵 ) = ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) |
31 |
25 30
|
eqtri |
⊢ ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 = ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) |
32 |
|
iuneq1 |
⊢ ( 𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵 ) |
33 |
|
0iun |
⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅ |
34 |
33
|
a1i |
⊢ ( 𝑤 = ∅ → ∪ 𝑥 ∈ ∅ 𝐵 = ∅ ) |
35 |
32 34
|
eqtrd |
⊢ ( 𝑤 = ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 = ∅ ) |
36 |
35
|
uneq1d |
⊢ ( 𝑤 = ∅ → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) = ( ∅ ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ) |
37 |
|
0un |
⊢ ( ∅ ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 |
38 |
|
unidm |
⊢ ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 |
39 |
37 38
|
eqtr4i |
⊢ ( ∅ ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) |
40 |
39
|
a1i |
⊢ ( 𝑤 = ∅ → ( ∅ ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ) |
41 |
36 40
|
eqtrd |
⊢ ( 𝑤 = ∅ → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ) |
42 |
41
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ 𝑤 = ∅ ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ) |
43 |
|
simpl |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) → 𝜑 ) |
44 |
|
eldifi |
⊢ ( 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) → 𝑢 ∈ 𝐴 ) |
45 |
44
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) → 𝑢 ∈ 𝐴 ) |
46 |
|
nfv |
⊢ Ⅎ 𝑥 𝑢 ∈ 𝐴 |
47 |
1 46
|
nfan |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) |
48 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐷 |
49 |
26 48
|
nfel |
⊢ Ⅎ 𝑥 ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 |
50 |
47 49
|
nfim |
⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) |
51 |
|
eleq1 |
⊢ ( 𝑥 = 𝑢 → ( 𝑥 ∈ 𝐴 ↔ 𝑢 ∈ 𝐴 ) ) |
52 |
51
|
anbi2d |
⊢ ( 𝑥 = 𝑢 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) ) ) |
53 |
28
|
eleq1d |
⊢ ( 𝑥 = 𝑢 → ( 𝐵 ∈ 𝐷 ↔ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) ) |
54 |
52 53
|
imbi12d |
⊢ ( 𝑥 = 𝑢 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) ) ) |
55 |
50 54 2
|
chvarfv |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) |
56 |
38 55
|
eqeltrid |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ) → ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
57 |
43 45 56
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) → ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
58 |
57
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ 𝑤 = ∅ ) → ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
59 |
42 58
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ 𝑤 = ∅ ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
60 |
59
|
adantlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) ∧ 𝑤 = ∅ ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
61 |
|
simplll |
⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) ∧ ¬ 𝑤 = ∅ ) → 𝜑 ) |
62 |
44
|
ad3antlr |
⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) ∧ ¬ 𝑤 = ∅ ) → 𝑢 ∈ 𝐴 ) |
63 |
|
neqne |
⊢ ( ¬ 𝑤 = ∅ → 𝑤 ≠ ∅ ) |
64 |
63
|
adantl |
⊢ ( ( ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ∧ ¬ 𝑤 = ∅ ) → 𝑤 ≠ ∅ ) |
65 |
|
simpl |
⊢ ( ( ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ∧ ¬ 𝑤 = ∅ ) → ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) |
66 |
64 65
|
mpd |
⊢ ( ( ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ∧ ¬ 𝑤 = ∅ ) → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) |
67 |
66
|
adantll |
⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) ∧ ¬ 𝑤 = ∅ ) → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) |
68 |
55
|
3adant3 |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) → ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) |
69 |
|
simp3 |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) |
70 |
|
simp1 |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) → 𝜑 ) |
71 |
70 69 68
|
3jca |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) → ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) ) |
72 |
|
eleq1 |
⊢ ( 𝑧 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 → ( 𝑧 ∈ 𝐷 ↔ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) ) |
73 |
72
|
3anbi3d |
⊢ ( 𝑧 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 → ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) ↔ ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) ) ) |
74 |
|
uneq2 |
⊢ ( 𝑧 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) = ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ) |
75 |
74
|
eleq1d |
⊢ ( 𝑧 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 → ( ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) ∈ 𝐷 ↔ ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) ) |
76 |
73 75
|
imbi12d |
⊢ ( 𝑧 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 → ( ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) ) ) |
77 |
76
|
imbi2d |
⊢ ( 𝑧 = ⦋ 𝑢 / 𝑥 ⦌ 𝐵 → ( ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) ∈ 𝐷 ) ) ↔ ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) ) ) ) |
78 |
|
eleq1 |
⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → ( 𝑦 ∈ 𝐷 ↔ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) |
79 |
78
|
3anbi2d |
⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) ↔ ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) ) ) |
80 |
|
uneq1 |
⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → ( 𝑦 ∪ 𝑧 ) = ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) ) |
81 |
80
|
eleq1d |
⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → ( ( 𝑦 ∪ 𝑧 ) ∈ 𝐷 ↔ ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) ∈ 𝐷 ) ) |
82 |
79 81
|
imbi12d |
⊢ ( 𝑦 = ∪ 𝑥 ∈ 𝑤 𝐵 → ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( 𝑦 ∪ 𝑧 ) ∈ 𝐷 ) ↔ ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) ∈ 𝐷 ) ) ) |
83 |
82 3
|
vtoclg |
⊢ ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ 𝑧 ) ∈ 𝐷 ) ) |
84 |
77 83
|
vtoclg |
⊢ ( ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 → ( ( 𝜑 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ∧ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) ) ) |
85 |
68 69 71 84
|
syl3c |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐴 ∧ ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
86 |
61 62 67 85
|
syl3anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) ∧ ¬ 𝑤 = ∅ ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
87 |
60 86
|
pm2.61dan |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) → ( ∪ 𝑥 ∈ 𝑤 𝐵 ∪ ⦋ 𝑢 / 𝑥 ⦌ 𝐵 ) ∈ 𝐷 ) |
88 |
31 87
|
eqeltrid |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) → ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 ∈ 𝐷 ) |
89 |
88
|
a1d |
⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ∧ ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) ) → ( ( 𝑤 ∪ { 𝑢 } ) ≠ ∅ → ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 ∈ 𝐷 ) ) |
90 |
89
|
ex |
⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) → ( ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) → ( ( 𝑤 ∪ { 𝑢 } ) ≠ ∅ → ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 ∈ 𝐷 ) ) ) |
91 |
90
|
adantrl |
⊢ ( ( 𝜑 ∧ ( 𝑤 ⊆ 𝐴 ∧ 𝑢 ∈ ( 𝐴 ∖ 𝑤 ) ) ) → ( ( 𝑤 ≠ ∅ → ∪ 𝑥 ∈ 𝑤 𝐵 ∈ 𝐷 ) → ( ( 𝑤 ∪ { 𝑢 } ) ≠ ∅ → ∪ 𝑥 ∈ ( 𝑤 ∪ { 𝑢 } ) 𝐵 ∈ 𝐷 ) ) ) |
92 |
9 13 17 21 24 91 4
|
findcard2d |
⊢ ( 𝜑 → ( 𝐴 ≠ ∅ → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 ) ) |
93 |
5 92
|
mpd |
⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 ) |