Metamath Proof Explorer

Theorem imasetpreimafvbijlemfo

Description: Lemma for imasetpreimafvbij : the mapping H is a function onto the range of function F . (Contributed by AV, 22-Mar-2024)

Ref Expression
Hypotheses fundcmpsurinj.p ⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
fundcmpsurinj.h ⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
Assertion imasetpreimafvbijlemfo ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 : 𝑃 –onto→ ( 𝐹 “ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p ⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2 fundcmpsurinj.h ⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
3 1 2 imasetpreimafvbijlemf ⊢ ( 𝐹 Fn 𝐴 → 𝐻 : 𝑃 ⟶ ( 𝐹 “ 𝐴 ) )
4 3 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 : 𝑃 ⟶ ( 𝐹 “ 𝐴 ) )
5 1 preimafvelsetpreimafv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ∈ 𝑃 )
6 5 3expa ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ∈ 𝑃 )
7 imaeq2 ⊢ ( 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ( 𝐹 “ 𝑝 ) = ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) )
8 7 unieqd ⊢ ( 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ∪ ( 𝐹 “ 𝑝 ) = ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) )
9 8 eqeq2d ⊢ ( 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ( ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ↔ ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) )
10 9 adantl ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) → ( ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ↔ ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) ) )
11 uniimaprimaeqfv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) = ( 𝐹 ‘ 𝑎 ) )
12 11 adantlr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) = ( 𝐹 ‘ 𝑎 ) )
13 12 eqcomd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) )
14 6 10 13 rspcedvd ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ∃ 𝑝 ∈ 𝑃 ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) )
15 eqeq1 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑎 ) → ( 𝑦 = ∪ ( 𝐹 “ 𝑝 ) ↔ ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ) )
16 15 eqcoms ⊢ ( ( 𝐹 ‘ 𝑎 ) = 𝑦 → ( 𝑦 = ∪ ( 𝐹 “ 𝑝 ) ↔ ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ) )
17 16 rexbidv ⊢ ( ( 𝐹 ‘ 𝑎 ) = 𝑦 → ( ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) ↔ ∃ 𝑝 ∈ 𝑃 ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ) )
18 14 17 syl5ibrcom ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑎 ) = 𝑦 → ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) ) )
19 18 rexlimdva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 → ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) ) )
20 8 eqcomd ⊢ ( 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) = ∪ ( 𝐹 “ 𝑝 ) )
21 13 20 sylan9eq ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ) → ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) )
22 21 ex ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ) )
23 22 reximdva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑎 ∈ 𝐴 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) → ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ) )
24 1 elsetpreimafv ⊢ ( 𝑝 ∈ 𝑃 → ∃ 𝑥 ∈ 𝐴 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
25 fveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑥 ) )
26 25 sneqd ⊢ ( 𝑎 = 𝑥 → { ( 𝐹 ‘ 𝑎 ) } = { ( 𝐹 ‘ 𝑥 ) } )
27 26 imaeq2d ⊢ ( 𝑎 = 𝑥 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
28 27 eqeq2d ⊢ ( 𝑎 = 𝑥 → ( 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ↔ 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
29 28 cbvrexvw ⊢ ( ∃ 𝑎 ∈ 𝐴 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) ↔ ∃ 𝑥 ∈ 𝐴 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
30 24 29 sylibr ⊢ ( 𝑝 ∈ 𝑃 → ∃ 𝑎 ∈ 𝐴 𝑝 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑎 ) } ) )
31 23 30 impel ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑝 ∈ 𝑃 ) → ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) )
32 eqeq2 ⊢ ( 𝑦 = ∪ ( 𝐹 “ 𝑝 ) → ( ( 𝐹 ‘ 𝑎 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ) )
33 32 rexbidv ⊢ ( 𝑦 = ∪ ( 𝐹 “ 𝑝 ) → ( ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 ↔ ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = ∪ ( 𝐹 “ 𝑝 ) ) )
34 31 33 syl5ibrcom ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑝 ∈ 𝑃 ) → ( 𝑦 = ∪ ( 𝐹 “ 𝑝 ) → ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 ) )
35 34 rexlimdva ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) → ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 ) )
36 19 35 impbid ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 ↔ ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) ) )
37 36 abbidv ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → { 𝑦 ∣ ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 } = { 𝑦 ∣ ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) } )
38 fnfun ⊢ ( 𝐹 Fn 𝐴 → Fun 𝐹 )
39 fndm ⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
40 eqimss2 ⊢ ( dom 𝐹 = 𝐴 → 𝐴 ⊆ dom 𝐹 )
41 39 40 syl ⊢ ( 𝐹 Fn 𝐴 → 𝐴 ⊆ dom 𝐹 )
42 38 41 jca ⊢ ( 𝐹 Fn 𝐴 → ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) )
43 42 adantr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) )
44 dfimafn ⊢ ( ( Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 } )
45 43 44 syl ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 “ 𝐴 ) = { 𝑦 ∣ ∃ 𝑎 ∈ 𝐴 ( 𝐹 ‘ 𝑎 ) = 𝑦 } )
46 2 rnmpt ⊢ ran 𝐻 = { 𝑦 ∣ ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) }
47 46 a1i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ran 𝐻 = { 𝑦 ∣ ∃ 𝑝 ∈ 𝑃 𝑦 = ∪ ( 𝐹 “ 𝑝 ) } )
48 37 45 47 3eqtr4rd ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → ran 𝐻 = ( 𝐹 “ 𝐴 ) )
49 dffo2 ⊢ ( 𝐻 : 𝑃 –onto→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐻 : 𝑃 ⟶ ( 𝐹 “ 𝐴 ) ∧ ran 𝐻 = ( 𝐹 “ 𝐴 ) ) )
50 4 48 49 sylanbrc ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐴 ∈ 𝑉 ) → 𝐻 : 𝑃 –onto→ ( 𝐹 “ 𝐴 ) )