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	biimpi	⊢ ( 𝐹 Fn 𝐴 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
3	2	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ ran 𝐹 )
4		cnvimass	⊢ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ dom 𝐹
5		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6	4 5	sseqtrid	⊢ ( 𝐹 Fn 𝐴 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 )
7	6	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 )
8		preimafvsnel	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) )
9	3 7 8	3jca	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 ∧ 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) )
10		fniniseg	⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
11	10	adantr	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) ) )
12		simpr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
13	11 12	biimtrdi	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) ) )
14	13	ralrimiv	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
15		uniimafveqt	⊢ ( ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ⊆ 𝐴 ∧ 𝑋 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) → ( ∀ 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) = ( 𝐹 ‘ 𝑋 ) ) )
16	9 14 15	sylc	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∪ ( 𝐹 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑋 ) } ) ) = ( 𝐹 ‘ 𝑋 ) )