Theorem unipreima

Description: Preimage of a class union. (Contributed by Thierry Arnoux, 7-Feb-2017)

	Ref	Expression
Assertion	unipreima	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2		r19.42v	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) )
3	2	bicomi	⊢ ( ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) )
4	3	a1i	⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
5		eluni2	⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 )
6	5	anbi2i	⊢ ( ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) )
7	6	a1i	⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
8		elpreima	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
9	8	rexbidv	⊢ ( 𝐹 Fn dom 𝐹 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) ) )
10	4 7 9	3bitr4d	⊢ ( 𝐹 Fn dom 𝐹 → ( ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
11		elpreima	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ( ◡ 𝐹 “ ∪ 𝐴 ) ↔ ( 𝑦 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐴 ) ) )
12		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) )
13	12	a1i	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
14	10 11 13	3bitr4d	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑦 ∈ ( ◡ 𝐹 “ ∪ 𝐴 ) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) ) )
15	14	eqrdv	⊢ ( 𝐹 Fn dom 𝐹 → ( ◡ 𝐹 “ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )
16	1 15	sylbi	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝑥 ) )