Theorem disjpreima

Description: A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017)

	Ref	Expression
Assertion	disjpreima	⊢ ( ( Fun 𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) → Disj 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		inpreima	⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) = ( ( ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∩ ( ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
2		imaeq2	⊢ ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ → ( ◡ 𝐹 “ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) = ( ◡ 𝐹 “ ∅ ) )
3		ima0	⊢ ( ◡ 𝐹 “ ∅ ) = ∅
4	2 3	eqtrdi	⊢ ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ → ( ◡ 𝐹 “ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) = ∅ )
5	1 4	sylan9req	⊢ ( ( Fun 𝐹 ∧ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ( ( ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∩ ( ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) = ∅ )
6	5	ex	⊢ ( Fun 𝐹 → ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ → ( ( ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∩ ( ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) = ∅ ) )
7		csbima12	⊢ ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) = ( ⦋ 𝑦 / 𝑥 ⦌ ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
8		csbconstg	⊢ ( 𝑦 ∈ V → ⦋ 𝑦 / 𝑥 ⦌ ◡ 𝐹 = ◡ 𝐹 )
9	8	elv	⊢ ⦋ 𝑦 / 𝑥 ⦌ ◡ 𝐹 = ◡ 𝐹
10	9	imaeq1i	⊢ ( ⦋ 𝑦 / 𝑥 ⦌ ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
11	7 10	eqtri	⊢ ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) = ( ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
12		csbima12	⊢ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) = ( ⦋ 𝑧 / 𝑥 ⦌ ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
13		csbconstg	⊢ ( 𝑧 ∈ V → ⦋ 𝑧 / 𝑥 ⦌ ◡ 𝐹 = ◡ 𝐹 )
14	13	elv	⊢ ⦋ 𝑧 / 𝑥 ⦌ ◡ 𝐹 = ◡ 𝐹
15	14	imaeq1i	⊢ ( ⦋ 𝑧 / 𝑥 ⦌ ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ( ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
16	12 15	eqtri	⊢ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) = ( ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
17	11 16	ineq12i	⊢ ( ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ) = ( ( ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∩ ( ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
18	17	eqeq1i	⊢ ( ( ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ ↔ ( ( ◡ 𝐹 “ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ∩ ( ◡ 𝐹 “ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) = ∅ )
19	6 18	imbitrrdi	⊢ ( Fun 𝐹 → ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ → ( ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ ) )
20	19	orim2d	⊢ ( Fun 𝐹 → ( ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ ) ) )
21	20	ralimdv	⊢ ( Fun 𝐹 → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ ) ) )
22	21	ralimdv	⊢ ( Fun 𝐹 → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ ) ) )
23		disjors	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
24		disjors	⊢ ( Disj 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( ◡ 𝐹 “ 𝐵 ) ) = ∅ ) )
25	22 23 24	3imtr4g	⊢ ( Fun 𝐹 → ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) ) )
26	25	imp	⊢ ( ( Fun 𝐹 ∧ Disj 𝑥 ∈ 𝐴 𝐵 ) → Disj 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) )