Metamath Proof Explorer

Theorem uniimaprimaeqfv

Description: The union of the image of the preimage of a function value is the function value. (Contributed by AV, 12-Mar-2024)

Ref Expression
Assertion uniimaprimaeqfv ⊢ F Fn A ∧ X ∈ A → ⋃ F F -1 F ⁡ X = F ⁡ X

Proof

Step Hyp Ref Expression
1 dffn3 ⊢ F Fn A ↔ F : A ⟶ ran ⁡ F
2 1 birani ⊢ F Fn A ∧ X ∈ A → F : A ⟶ ran ⁡ F
3 cnvimass ⊢ F -1 F ⁡ X ⊆ dom ⁡ F
4 fndm ⊢ F Fn A → dom ⁡ F = A
5 3 4 sseqtrid ⊢ F Fn A → F -1 F ⁡ X ⊆ A
6 5 adantr ⊢ F Fn A ∧ X ∈ A → F -1 F ⁡ X ⊆ A
7 preimafvsnel ⊢ F Fn A ∧ X ∈ A → X ∈ F -1 F ⁡ X
8 2 6 7 3jca ⊢ F Fn A ∧ X ∈ A → F : A ⟶ ran ⁡ F ∧ F -1 F ⁡ X ⊆ A ∧ X ∈ F -1 F ⁡ X
9 fniniseg ⊢ F Fn A → x ∈ F -1 F ⁡ X ↔ x ∈ A ∧ F ⁡ x = F ⁡ X
10 9 adantr ⊢ F Fn A ∧ X ∈ A → x ∈ F -1 F ⁡ X ↔ x ∈ A ∧ F ⁡ x = F ⁡ X
11 simpr ⊢ x ∈ A ∧ F ⁡ x = F ⁡ X → F ⁡ x = F ⁡ X
12 10 11 biimtrdi ⊢ F Fn A ∧ X ∈ A → x ∈ F -1 F ⁡ X → F ⁡ x = F ⁡ X
13 12 ralrimiv ⊢ F Fn A ∧ X ∈ A → ∀ x ∈ F -1 F ⁡ X F ⁡ x = F ⁡ X
14 uniimafveqt ⊢ F : A ⟶ ran ⁡ F ∧ F -1 F ⁡ X ⊆ A ∧ X ∈ F -1 F ⁡ X → ∀ x ∈ F -1 F ⁡ X F ⁡ x = F ⁡ X → ⋃ F F -1 F ⁡ X = F ⁡ X
15 8 13 14 sylc ⊢ F Fn A ∧ X ∈ A → ⋃ F F -1 F ⁡ X = F ⁡ X