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⁡F∧Disjx∈AB→Disjx∈AF-1B

Proof

Step Hyp Ref Expression
1 inpreima ⊢Fun⁡F→F-1⦋y/x⦌B∩⦋z/x⦌B=F-1⦋y/x⦌B∩F-1⦋z/x⦌B
2 imaeq2 ⊢⦋y/x⦌B∩⦋z/x⦌B=∅→F-1⦋y/x⦌B∩⦋z/x⦌B=F-1∅
3 ima0 ⊢F-1∅=∅
4 2 3 eqtrdi ⊢⦋y/x⦌B∩⦋z/x⦌B=∅→F-1⦋y/x⦌B∩⦋z/x⦌B=∅
5 1 4 sylan9req ⊢Fun⁡F∧⦋y/x⦌B∩⦋z/x⦌B=∅→F-1⦋y/x⦌B∩F-1⦋z/x⦌B=∅
6 5 ex ⊢Fun⁡F→⦋y/x⦌B∩⦋z/x⦌B=∅→F-1⦋y/x⦌B∩F-1⦋z/x⦌B=∅
7 csbima12 ⊢⦋y/x⦌F-1B=⦋y/x⦌F-1⦋y/x⦌B
8 csbconstg ⊢y∈V→⦋y/x⦌F-1=F-1
9 8 elv ⊢⦋y/x⦌F-1=F-1
10 9 imaeq1i ⊢⦋y/x⦌F-1⦋y/x⦌B=F-1⦋y/x⦌B
11 7 10 eqtri ⊢⦋y/x⦌F-1B=F-1⦋y/x⦌B
12 csbima12 ⊢⦋z/x⦌F-1B=⦋z/x⦌F-1⦋z/x⦌B
13 csbconstg ⊢z∈V→⦋z/x⦌F-1=F-1
14 13 elv ⊢⦋z/x⦌F-1=F-1
15 14 imaeq1i ⊢⦋z/x⦌F-1⦋z/x⦌B=F-1⦋z/x⦌B
16 12 15 eqtri ⊢⦋z/x⦌F-1B=F-1⦋z/x⦌B
17 11 16 ineq12i ⊢⦋y/x⦌F-1B∩⦋z/x⦌F-1B=F-1⦋y/x⦌B∩F-1⦋z/x⦌B
18 17 eqeq1i ⊢⦋y/x⦌F-1B∩⦋z/x⦌F-1B=∅↔F-1⦋y/x⦌B∩F-1⦋z/x⦌B=∅
19 6 18 syl6ibr ⊢Fun⁡F→⦋y/x⦌B∩⦋z/x⦌B=∅→⦋y/x⦌F-1B∩⦋z/x⦌F-1B=∅
20 19 orim2d ⊢Fun⁡F→y=z∨⦋y/x⦌B∩⦋z/x⦌B=∅→y=z∨⦋y/x⦌F-1B∩⦋z/x⦌F-1B=∅
21 20 ralimdv ⊢Fun⁡F→∀z∈Ay=z∨⦋y/x⦌B∩⦋z/x⦌B=∅→∀z∈Ay=z∨⦋y/x⦌F-1B∩⦋z/x⦌F-1B=∅
22 21 ralimdv ⊢Fun⁡F→∀y∈A∀z∈Ay=z∨⦋y/x⦌B∩⦋z/x⦌B=∅→∀y∈A∀z∈Ay=z∨⦋y/x⦌F-1B∩⦋z/x⦌F-1B=∅
23 disjors ⊢Disjx∈AB↔∀y∈A∀z∈Ay=z∨⦋y/x⦌B∩⦋z/x⦌B=∅
24 disjors ⊢Disjx∈AF-1B↔∀y∈A∀z∈Ay=z∨⦋y/x⦌F-1B∩⦋z/x⦌F-1B=∅
25 22 23 24 3imtr4g ⊢Fun⁡F→Disjx∈AB→Disjx∈AF-1B
26 25 imp ⊢Fun⁡F∧Disjx∈AB→Disjx∈AF-1B