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 biimpi ⊢ F Fn A → F : A ⟶ ran ⁡ F
3 2 adantr ⊢ F Fn A ∧ X ∈ A → F : A ⟶ ran ⁡ F
4 cnvimass ⊢ F -1 F ⁡ X ⊆ dom ⁡ F
5 fndm ⊢ F Fn A → dom ⁡ F = A
6 4 5 sseqtrid ⊢ F Fn A → F -1 F ⁡ X ⊆ A
7 6 adantr ⊢ F Fn A ∧ X ∈ A → F -1 F ⁡ X ⊆ A
8 preimafvsnel ⊢ F Fn A ∧ X ∈ A → X ∈ F -1 F ⁡ X
9 3 7 8 3jca ⊢ F Fn A ∧ X ∈ A → F : A ⟶ ran ⁡ F ∧ F -1 F ⁡ X ⊆ A ∧ X ∈ F -1 F ⁡ X
10 fniniseg ⊢ F Fn A → x ∈ F -1 F ⁡ X ↔ x ∈ A ∧ F ⁡ x = F ⁡ X
11 10 adantr ⊢ F Fn A ∧ X ∈ A → x ∈ F -1 F ⁡ X ↔ x ∈ A ∧ F ⁡ x = F ⁡ X
12 simpr ⊢ x ∈ A ∧ F ⁡ x = F ⁡ X → F ⁡ x = F ⁡ X
13 11 12 syl6bi ⊢ F Fn A ∧ X ∈ A → x ∈ F -1 F ⁡ X → F ⁡ x = F ⁡ X
14 13 ralrimiv ⊢ F Fn A ∧ X ∈ A → ∀ x ∈ F -1 F ⁡ X F ⁡ x = F ⁡ X
15 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
16 9 14 15 sylc ⊢ F Fn A ∧ X ∈ A → ⋃ F F -1 F ⁡ X = F ⁡ X