Metamath Proof Explorer

Theorem imasetpreimafvbijlemf1

Description: Lemma for imasetpreimafvbij : the mapping H is an injective function into the range of function F . (Contributed by AV, 9-Mar-2024) (Revised by AV, 22-Mar-2024)

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

Proof

Step Hyp Ref Expression
1 fundcmpsurinj.p ⊢ 𝑃 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) }
2 fundcmpsurinj.h ⊢ 𝐻 = ( 𝑝 ∈ 𝑃 ↦ ∪ ( 𝐹 “ 𝑝 ) )
3 1 2 imasetpreimafvbijlemf ⊢ ( 𝐹 Fn 𝐴 → 𝐻 : 𝑃 ⟶ ( 𝐹 “ 𝐴 ) )
4 1 2 imasetpreimafvbijlemfv1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑠 ∈ 𝑃 ) → ∃ 𝑏 ∈ 𝑠 ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) )
5 1 2 imasetpreimafvbijlemfv1 ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑟 ∈ 𝑃 ) → ∃ 𝑎 ∈ 𝑟 ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) )
6 4 5 anim12dan ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( ∃ 𝑏 ∈ 𝑠 ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) ∧ ∃ 𝑎 ∈ 𝑟 ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) ) )
7 eqeq12 ⊢ ( ( ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) ↔ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) )
8 7 ancoms ⊢ ( ( ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) ↔ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) )
9 8 adantl ⊢ ( ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) ∧ ( ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) ) ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) ↔ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) )
10 simplll ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) → 𝐹 Fn 𝐴 )
11 simpllr ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) → ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) )
12 simpr ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) → 𝑏 ∈ 𝑠 )
13 12 anim1i ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) → ( 𝑏 ∈ 𝑠 ∧ 𝑎 ∈ 𝑟 ) )
14 1 elsetpreimafveq ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ∧ ( 𝑏 ∈ 𝑠 ∧ 𝑎 ∈ 𝑟 ) ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) → 𝑠 = 𝑟 ) )
15 10 11 13 14 syl3anc ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) → 𝑠 = 𝑟 ) )
16 15 adantr ⊢ ( ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) ∧ ( ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) ) ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) → 𝑠 = 𝑟 ) )
17 9 16 sylbid ⊢ ( ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) ∧ ( ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) ) ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) )
18 17 exp32 ⊢ ( ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) ∧ 𝑎 ∈ 𝑟 ) → ( ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) ) ) )
19 18 rexlimdva ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) → ( ∃ 𝑎 ∈ 𝑟 ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) ) ) )
20 19 com23 ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) ∧ 𝑏 ∈ 𝑠 ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) → ( ∃ 𝑎 ∈ 𝑟 ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) ) ) )
21 20 rexlimdva ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( ∃ 𝑏 ∈ 𝑠 ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) → ( ∃ 𝑎 ∈ 𝑟 ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) ) ) )
22 21 impd ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( ( ∃ 𝑏 ∈ 𝑠 ( 𝐻 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑏 ) ∧ ∃ 𝑎 ∈ 𝑟 ( 𝐻 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) ) )
23 6 22 mpd ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝑠 ∈ 𝑃 ∧ 𝑟 ∈ 𝑃 ) ) → ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) )
24 23 ralrimivva ⊢ ( 𝐹 Fn 𝐴 → ∀ 𝑠 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) )
25 dff13 ⊢ ( 𝐻 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) ↔ ( 𝐻 : 𝑃 ⟶ ( 𝐹 “ 𝐴 ) ∧ ∀ 𝑠 ∈ 𝑃 ∀ 𝑟 ∈ 𝑃 ( ( 𝐻 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑟 ) → 𝑠 = 𝑟 ) ) )
26 3 24 25 sylanbrc ⊢ ( 𝐹 Fn 𝐴 → 𝐻 : 𝑃 –1-1→ ( 𝐹 “ 𝐴 ) )