Metamath Proof Explorer

Theorem disjrnmpt2

Description: Disjointness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis disjrnmpt2.1 ⊢F=x∈A⟼B
Assertion disjrnmpt2 ⊢Disjx∈AB→Disjy∈ran⁡Fy

Proof

Step Hyp Ref Expression
1 disjrnmpt2.1 ⊢F=x∈A⟼B
2 id ⊢y=w→y=w
3 2 cbvdisjv ⊢Disjy∈ran⁡Fy↔Disjw∈ran⁡Fw
4 id ⊢w=v→w=v
5 4 ndisj2 ⊢¬Disjw∈ran⁡Fw↔∃w∈ran⁡F∃v∈ran⁡Fw≠v∧w∩v≠∅
6 5 biimpi ⊢¬Disjw∈ran⁡Fw→∃w∈ran⁡F∃v∈ran⁡Fw≠v∧w∩v≠∅
7 3 6 sylnbi ⊢¬Disjy∈ran⁡Fy→∃w∈ran⁡F∃v∈ran⁡Fw≠v∧w∩v≠∅
8 1 elrnmpt ⊢w∈ran⁡F→w∈ran⁡F↔∃x∈Aw=B
9 8 ibi ⊢w∈ran⁡F→∃x∈Aw=B
10 nfcv ⊢Ⅎ_zB
11 nfcsb1v ⊢Ⅎ_x⦋z/x⦌B
12 csbeq1a ⊢x=z→B=⦋z/x⦌B
13 10 11 12 cbvmpt ⊢x∈A⟼B=z∈A⟼⦋z/x⦌B
14 1 13 eqtri ⊢F=z∈A⟼⦋z/x⦌B
15 14 elrnmpt ⊢v∈ran⁡F→v∈ran⁡F↔∃z∈Av=⦋z/x⦌B
16 15 ibi ⊢v∈ran⁡F→∃z∈Av=⦋z/x⦌B
17 9 16 anim12i ⊢w∈ran⁡F∧v∈ran⁡F→∃x∈Aw=B∧∃z∈Av=⦋z/x⦌B
18 nfv ⊢Ⅎzw=B
19 11 nfeq2 ⊢Ⅎxv=⦋z/x⦌B
20 18 19 reean ⊢∃x∈A∃z∈Aw=B∧v=⦋z/x⦌B↔∃x∈Aw=B∧∃z∈Av=⦋z/x⦌B
21 17 20 sylibr ⊢w∈ran⁡F∧v∈ran⁡F→∃x∈A∃z∈Aw=B∧v=⦋z/x⦌B
22 21 adantr ⊢w∈ran⁡F∧v∈ran⁡F∧w≠v∧w∩v≠∅→∃x∈A∃z∈Aw=B∧v=⦋z/x⦌B
23 nfmpt1 ⊢Ⅎ_xx∈A⟼B
24 1 23 nfcxfr ⊢Ⅎ_xF
25 24 nfrn ⊢Ⅎ_xran⁡F
26 25 nfcri ⊢Ⅎxw∈ran⁡F
27 25 nfcri ⊢Ⅎxv∈ran⁡F
28 26 27 nfan ⊢Ⅎxw∈ran⁡F∧v∈ran⁡F
29 nfv ⊢Ⅎxw≠v∧w∩v≠∅
30 28 29 nfan ⊢Ⅎxw∈ran⁡F∧v∈ran⁡F∧w≠v∧w∩v≠∅
31 simpll ⊢w=B∧v=⦋z/x⦌B∧x=z→w=B
32 12 adantl ⊢w=B∧v=⦋z/x⦌B∧x=z→B=⦋z/x⦌B
33 id ⊢v=⦋z/x⦌B→v=⦋z/x⦌B
34 33 eqcomd ⊢v=⦋z/x⦌B→⦋z/x⦌B=v
35 34 ad2antlr ⊢w=B∧v=⦋z/x⦌B∧x=z→⦋z/x⦌B=v
36 31 32 35 3eqtrd ⊢w=B∧v=⦋z/x⦌B∧x=z→w=v
37 36 adantll ⊢w≠v∧w=B∧v=⦋z/x⦌B∧x=z→w=v
38 simpll ⊢w≠v∧w=B∧v=⦋z/x⦌B∧x=z→w≠v
39 38 neneqd ⊢w≠v∧w=B∧v=⦋z/x⦌B∧x=z→¬w=v
40 37 39 pm2.65da ⊢w≠v∧w=B∧v=⦋z/x⦌B→¬x=z
41 40 neqned ⊢w≠v∧w=B∧v=⦋z/x⦌B→x≠z
42 41 adantlr ⊢w≠v∧w∩v≠∅∧w=B∧v=⦋z/x⦌B→x≠z
43 id ⊢w=B→w=B
44 43 eqcomd ⊢w=B→B=w
45 44 ad2antrl ⊢w∩v≠∅∧w=B∧v=⦋z/x⦌B→B=w
46 34 ad2antll ⊢w∩v≠∅∧w=B∧v=⦋z/x⦌B→⦋z/x⦌B=v
47 45 46 ineq12d ⊢w∩v≠∅∧w=B∧v=⦋z/x⦌B→B∩⦋z/x⦌B=w∩v
48 simpl ⊢w∩v≠∅∧w=B∧v=⦋z/x⦌B→w∩v≠∅
49 47 48 eqnetrd ⊢w∩v≠∅∧w=B∧v=⦋z/x⦌B→B∩⦋z/x⦌B≠∅
50 49 adantll ⊢w≠v∧w∩v≠∅∧w=B∧v=⦋z/x⦌B→B∩⦋z/x⦌B≠∅
51 42 50 jca ⊢w≠v∧w∩v≠∅∧w=B∧v=⦋z/x⦌B→x≠z∧B∩⦋z/x⦌B≠∅
52 51 ex ⊢w≠v∧w∩v≠∅→w=B∧v=⦋z/x⦌B→x≠z∧B∩⦋z/x⦌B≠∅
53 52 adantl ⊢w∈ran⁡F∧v∈ran⁡F∧w≠v∧w∩v≠∅→w=B∧v=⦋z/x⦌B→x≠z∧B∩⦋z/x⦌B≠∅
54 53 reximdv ⊢w∈ran⁡F∧v∈ran⁡F∧w≠v∧w∩v≠∅→∃z∈Aw=B∧v=⦋z/x⦌B→∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
55 54 a1d ⊢w∈ran⁡F∧v∈ran⁡F∧w≠v∧w∩v≠∅→x∈A→∃z∈Aw=B∧v=⦋z/x⦌B→∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
56 30 55 reximdai ⊢w∈ran⁡F∧v∈ran⁡F∧w≠v∧w∩v≠∅→∃x∈A∃z∈Aw=B∧v=⦋z/x⦌B→∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
57 22 56 mpd ⊢w∈ran⁡F∧v∈ran⁡F∧w≠v∧w∩v≠∅→∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
58 57 ex ⊢w∈ran⁡F∧v∈ran⁡F→w≠v∧w∩v≠∅→∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
59 58 a1i ⊢¬Disjy∈ran⁡Fy→w∈ran⁡F∧v∈ran⁡F→w≠v∧w∩v≠∅→∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
60 59 rexlimdvv ⊢¬Disjy∈ran⁡Fy→∃w∈ran⁡F∃v∈ran⁡Fw≠v∧w∩v≠∅→∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
61 7 60 mpd ⊢¬Disjy∈ran⁡Fy→∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
62 csbeq1 ⊢u=z→⦋u/x⦌B=⦋z/x⦌B
63 62 ndisj2 ⊢¬Disju∈A⦋u/x⦌B↔∃u∈A∃z∈Au≠z∧⦋u/x⦌B∩⦋z/x⦌B≠∅
64 nfcv ⊢Ⅎ_xA
65 nfv ⊢Ⅎxu≠z
66 nfcsb1v ⊢Ⅎ_x⦋u/x⦌B
67 66 11 nfin ⊢Ⅎ_x⦋u/x⦌B∩⦋z/x⦌B
68 nfcv ⊢Ⅎ_x∅
69 67 68 nfne ⊢Ⅎx⦋u/x⦌B∩⦋z/x⦌B≠∅
70 65 69 nfan ⊢Ⅎxu≠z∧⦋u/x⦌B∩⦋z/x⦌B≠∅
71 64 70 nfrexw ⊢Ⅎx∃z∈Au≠z∧⦋u/x⦌B∩⦋z/x⦌B≠∅
72 nfv ⊢Ⅎu∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
73 neeq1 ⊢u=x→u≠z↔x≠z
74 csbeq1 ⊢u=x→⦋u/x⦌B=⦋x/x⦌B
75 csbid ⊢⦋x/x⦌B=B
76 74 75 eqtrdi ⊢u=x→⦋u/x⦌B=B
77 76 ineq1d ⊢u=x→⦋u/x⦌B∩⦋z/x⦌B=B∩⦋z/x⦌B
78 77 neeq1d ⊢u=x→⦋u/x⦌B∩⦋z/x⦌B≠∅↔B∩⦋z/x⦌B≠∅
79 73 78 anbi12d ⊢u=x→u≠z∧⦋u/x⦌B∩⦋z/x⦌B≠∅↔x≠z∧B∩⦋z/x⦌B≠∅
80 79 rexbidv ⊢u=x→∃z∈Au≠z∧⦋u/x⦌B∩⦋z/x⦌B≠∅↔∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
81 71 72 80 cbvrexw ⊢∃u∈A∃z∈Au≠z∧⦋u/x⦌B∩⦋z/x⦌B≠∅↔∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
82 63 81 bitri ⊢¬Disju∈A⦋u/x⦌B↔∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
83 nfcv ⊢Ⅎ_uB
84 csbeq1a ⊢x=u→B=⦋u/x⦌B
85 83 66 84 cbvdisj ⊢Disjx∈AB↔Disju∈A⦋u/x⦌B
86 82 85 xchnxbir ⊢¬Disjx∈AB↔∃x∈A∃z∈Ax≠z∧B∩⦋z/x⦌B≠∅
87 61 86 sylibr ⊢¬Disjy∈ran⁡Fy→¬Disjx∈AB
88 87 con4i ⊢Disjx∈AB→Disjy∈ran⁡Fy