This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fiiuncl

Description: If a set is closed under the union of two sets, then it is closed under finite indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fiiuncl.xph ⊢ Ⅎ 𝑥 𝜑
fiiuncl.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐷 )
fiiuncl.un ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → ( 𝑦 ∪ 𝑧 ) ∈ 𝐷 )
fiiuncl.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fiiuncl.n0 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion fiiuncl ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 )

Proof

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 ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐷 )