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

Metamath Proof Explorer

Theorem founiiun0

Description: Union expressed as an indexed union, when a map onto is given. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion founiiun0 ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 uniiun ⊢ ∪ 𝐵 = ∪ 𝑦 ∈ 𝐵 𝑦
2 elun1 ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 𝐵 ∪ { ∅ } ) )
3 foelcdmi ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑦 ∈ ( 𝐵 ∪ { ∅ } ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
4 2 3 sylan2 ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
5 eqimss2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
6 5 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
7 4 6 syl ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
8 7 ralrimiva ⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) )
9 iunss2 ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑦 ⊆ ( 𝐹 ‘ 𝑥 ) → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )
10 8 9 syl ⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝑦 ∈ 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )
11 simpl ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) )
12 uneq1 ⊢ ( 𝐵 = ∅ → ( 𝐵 ∪ { ∅ } ) = ( ∅ ∪ { ∅ } ) )
13 0un ⊢ ( ∅ ∪ { ∅ } ) = { ∅ }
14 12 13 eqtrdi ⊢ ( 𝐵 = ∅ → ( 𝐵 ∪ { ∅ } ) = { ∅ } )
15 14 adantl ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → ( 𝐵 ∪ { ∅ } ) = { ∅ } )
16 foeq3 ⊢ ( ( 𝐵 ∪ { ∅ } ) = { ∅ } → ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ↔ 𝐹 : 𝐴 –onto→ { ∅ } ) )
17 15 16 syl ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ↔ 𝐹 : 𝐴 –onto→ { ∅ } ) )
18 11 17 mpbid ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → 𝐹 : 𝐴 –onto→ { ∅ } )
19 founiiun ⊢ ( 𝐹 : 𝐴 –onto→ { ∅ } → ∪ { ∅ } = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )
20 unisn0 ⊢ ∪ { ∅ } = ∅
21 19 20 eqtr3di ⊢ ( 𝐹 : 𝐴 –onto→ { ∅ } → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ∅ )
22 0ss ⊢ ∅ ⊆ ∪ 𝑦 ∈ 𝐵 𝑦
23 21 22 eqsstrdi ⊢ ( 𝐹 : 𝐴 –onto→ { ∅ } → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 )
24 18 23 syl ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝐵 = ∅ ) → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 )
25 ssid ⊢ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 )
26 sseq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) )
27 26 rspcev ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
28 25 27 mpan2 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
29 28 adantl ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
30 fof ⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → 𝐹 : 𝐴 ⟶ ( 𝐵 ∪ { ∅ } ) )
31 30 ffvelcdmda ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 ∪ { ∅ } ) )
32 elunnel1 ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐵 ∪ { ∅ } ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ { ∅ } )
33 31 32 sylan ⊢ ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ { ∅ } )
34 elsni ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { ∅ } → ( 𝐹 ‘ 𝑥 ) = ∅ )
35 33 34 syl ⊢ ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
36 35 adantllr ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
37 neq0 ⊢ ( ¬ 𝐵 = ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 )
38 37 biimpi ⊢ ( ¬ 𝐵 = ∅ → ∃ 𝑦 𝑦 ∈ 𝐵 )
39 38 adantr ⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 𝑦 ∈ 𝐵 )
40 id ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝐹 ‘ 𝑥 ) = ∅ )
41 0ss ⊢ ∅ ⊆ 𝑦
42 40 41 eqsstrdi ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
43 42 anim1ci ⊢ ( ( ( 𝐹 ‘ 𝑥 ) = ∅ ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) )
44 43 ex ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) )
45 44 adantl ⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) )
46 45 eximdv ⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ( ∃ 𝑦 𝑦 ∈ 𝐵 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) ) )
47 39 46 mpd ⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) )
48 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 ) )
49 47 48 sylibr ⊢ ( ( ¬ 𝐵 = ∅ ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
50 49 ad4ant24 ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
51 36 50 syldan ⊢ ( ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
52 29 51 pm2.61dan ⊢ ( ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
53 52 ralrimiva ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 )
54 iunss2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) ⊆ 𝑦 → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 )
55 53 54 syl ⊢ ( ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) ∧ ¬ 𝐵 = ∅ ) → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 )
56 24 55 pm2.61dan ⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 𝑦 )
57 10 56 eqssd ⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝑦 ∈ 𝐵 𝑦 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )
58 1 57 eqtrid ⊢ ( 𝐹 : 𝐴 –onto→ ( 𝐵 ∪ { ∅ } ) → ∪ 𝐵 = ∪ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) )