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 foelrni ( ( 𝐹 : 𝐴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 ffvelrnda ( ( 𝐹 : 𝐴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 syl5eq ( 𝐹 : 𝐴onto→ ( 𝐵 ∪ { ∅ } ) → 𝐵 = 𝑥𝐴 ( 𝐹𝑥 ) )