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	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		dffn3	⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
2	1	birani	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
3		cnvimass	⊢ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ dom 𝐹
4		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
5	3 4	sseqtrid	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 )
6	5	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 )
7		preimafvsnel	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) )
8	2 6 7	3jca	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 ∧ 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) )
9		fniniseg	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
10	9	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
11		simpr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
12	10 11	biimtrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) )
13	12	ralrimiv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
14		uniimafveqt	⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 ∧ 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) → ( ∀ 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) = ( 𝐹 ‘ 𝑋 ) ) )
15	8 13 14	sylc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) = ( 𝐹 ‘ 𝑋 ) )