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 ( 𝜑 𝑥𝐴 𝐵𝐷 )