Metamath Proof Explorer

Theorem iunxdif3

Description: An indexed union where some terms are the empty set. See iunxdif2 . (Contributed by Thierry Arnoux, 4-May-2020)

Ref Expression
Hypothesis iunxdif3.1 ⊢ Ⅎ 𝑥 𝐸
Assertion iunxdif3 ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 iunxdif3.1 ⊢ Ⅎ 𝑥 𝐸
2 inss2 ⊢ ( 𝐴 ∩ 𝐸 ) ⊆ 𝐸
3 nfcv ⊢ Ⅎ 𝑥 𝐴
4 3 1 nfin ⊢ Ⅎ 𝑥 ( 𝐴 ∩ 𝐸 )
5 4 1 ssrexf ⊢ ( ( 𝐴 ∩ 𝐸 ) ⊆ 𝐸 → ( ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ 𝐸 𝑦 ∈ 𝐵 ) )
6 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ↔ ∃ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝑦 ∈ 𝐵 )
7 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐸 𝐵 ↔ ∃ 𝑥 ∈ 𝐸 𝑦 ∈ 𝐵 )
8 5 6 7 3imtr4g ⊢ ( ( 𝐴 ∩ 𝐸 ) ⊆ 𝐸 → ( 𝑦 ∈ ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 → 𝑦 ∈ ∪ 𝑥 ∈ 𝐸 𝐵 ) )
9 8 ssrdv ⊢ ( ( 𝐴 ∩ 𝐸 ) ⊆ 𝐸 → ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ⊆ ∪ 𝑥 ∈ 𝐸 𝐵 )
10 2 9 ax-mp ⊢ ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ⊆ ∪ 𝑥 ∈ 𝐸 𝐵
11 iuneq2 ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐸 𝐵 = ∪ 𝑥 ∈ 𝐸 ∅ )
12 iun0 ⊢ ∪ 𝑥 ∈ 𝐸 ∅ = ∅
13 11 12 eqtrdi ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐸 𝐵 = ∅ )
14 10 13 sseqtrid ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ⊆ ∅ )
15 ss0 ⊢ ( ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ⊆ ∅ → ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 = ∅ )
16 14 15 syl ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 = ∅ )
17 16 uneq1d ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ( ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 ) = ( ∅ ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 ) )
18 iunxun ⊢ ∪ 𝑥 ∈ ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) 𝐵 = ( ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 )
19 inundif ⊢ ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) = 𝐴
20 19 nfth ⊢ Ⅎ 𝑥 ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) = 𝐴
21 3 1 nfdif ⊢ Ⅎ 𝑥 ( 𝐴 ∖ 𝐸 )
22 4 21 nfun ⊢ Ⅎ 𝑥 ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) )
23 id ⊢ ( ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) = 𝐴 → ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) = 𝐴 )
24 eqidd ⊢ ( ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) = 𝐴 → 𝐵 = 𝐵 )
25 20 22 3 23 24 iuneq12df ⊢ ( ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) = 𝐴 → ∪ 𝑥 ∈ ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 )
26 19 25 ax-mp ⊢ ∪ 𝑥 ∈ ( ( 𝐴 ∩ 𝐸 ) ∪ ( 𝐴 ∖ 𝐸 ) ) 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵
27 18 26 eqtr3i ⊢ ( ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 ) = ∪ 𝑥 ∈ 𝐴 𝐵
28 27 a1i ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ( ∪ 𝑥 ∈ ( 𝐴 ∩ 𝐸 ) 𝐵 ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 ) = ∪ 𝑥 ∈ 𝐴 𝐵 )
29 0un ⊢ ( ∅ ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 ) = ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵
30 29 a1i ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ( ∅ ∪ ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 ) = ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 )
31 17 28 30 3eqtr3rd ⊢ ( ∀ 𝑥 ∈ 𝐸 𝐵 = ∅ → ∪ 𝑥 ∈ ( 𝐴 ∖ 𝐸 ) 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵 )