Metamath Proof Explorer

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 syl6ibr ⊢ ( 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 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) )