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 e. A |-> B )
Assertion disjrnmpt2 
|- ( Disj_ x e. A B -> Disj_ y e. ran F y )

Proof

Step Hyp Ref Expression
1 disjrnmpt2.1 
 |-  F = ( x e. A |-> B )
2 id 
 |-  ( y = w -> y = w )
3 2 cbvdisjv 
 |-  ( Disj_ y e. ran F y <-> Disj_ w e. ran F w )
4 id 
 |-  ( w = v -> w = v )
5 4 ndisj2 
 |-  ( -. Disj_ w e. ran F w <-> E. w e. ran F E. v e. ran F ( w =/= v /\ ( w i^i v ) =/= (/) ) )
6 5 biimpi 
 |-  ( -. Disj_ w e. ran F w -> E. w e. ran F E. v e. ran F ( w =/= v /\ ( w i^i v ) =/= (/) ) )
7 3 6 sylnbi 
 |-  ( -. Disj_ y e. ran F y -> E. w e. ran F E. v e. ran F ( w =/= v /\ ( w i^i v ) =/= (/) ) )
8 1 elrnmpt 
 |-  ( w e. ran F -> ( w e. ran F <-> E. x e. A w = B ) )
9 8 ibi 
 |-  ( w e. ran F -> E. x e. A w = B )
10 nfcv 
 |-  F/_ z B
11 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
12 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
13 10 11 12 cbvmpt 
 |-  ( x e. A |-> B ) = ( z e. A |-> [_ z / x ]_ B )
14 1 13 eqtri 
 |-  F = ( z e. A |-> [_ z / x ]_ B )
15 14 elrnmpt 
 |-  ( v e. ran F -> ( v e. ran F <-> E. z e. A v = [_ z / x ]_ B ) )
16 15 ibi 
 |-  ( v e. ran F -> E. z e. A v = [_ z / x ]_ B )
17 9 16 anim12i 
 |-  ( ( w e. ran F /\ v e. ran F ) -> ( E. x e. A w = B /\ E. z e. A v = [_ z / x ]_ B ) )
18 nfv 
 |-  F/ z w = B
19 11 nfeq2 
 |-  F/ x v = [_ z / x ]_ B
20 18 19 reean 
 |-  ( E. x e. A E. z e. A ( w = B /\ v = [_ z / x ]_ B ) <-> ( E. x e. A w = B /\ E. z e. A v = [_ z / x ]_ B ) )
21 17 20 sylibr 
 |-  ( ( w e. ran F /\ v e. ran F ) -> E. x e. A E. z e. A ( w = B /\ v = [_ z / x ]_ B ) )
22 21 adantr 
 |-  ( ( ( w e. ran F /\ v e. ran F ) /\ ( w =/= v /\ ( w i^i v ) =/= (/) ) ) -> E. x e. A E. z e. A ( w = B /\ v = [_ z / x ]_ B ) )
23 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
24 1 23 nfcxfr 
 |-  F/_ x F
25 24 nfrn 
 |-  F/_ x ran F
26 25 nfcri 
 |-  F/ x w e. ran F
27 25 nfcri 
 |-  F/ x v e. ran F
28 26 27 nfan 
 |-  F/ x ( w e. ran F /\ v e. ran F )
29 nfv 
 |-  F/ x ( w =/= v /\ ( w i^i v ) =/= (/) )
30 28 29 nfan 
 |-  F/ x ( ( w e. ran F /\ v e. ran F ) /\ ( w =/= v /\ ( w i^i 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 i^i 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 i^i v ) =/= (/) /\ ( w = B /\ v = [_ z / x ]_ B ) ) -> B = w )
46 34 ad2antll 
 |-  ( ( ( w i^i v ) =/= (/) /\ ( w = B /\ v = [_ z / x ]_ B ) ) -> [_ z / x ]_ B = v )
47 45 46 ineq12d 
 |-  ( ( ( w i^i v ) =/= (/) /\ ( w = B /\ v = [_ z / x ]_ B ) ) -> ( B i^i [_ z / x ]_ B ) = ( w i^i v ) )
48 simpl 
 |-  ( ( ( w i^i v ) =/= (/) /\ ( w = B /\ v = [_ z / x ]_ B ) ) -> ( w i^i v ) =/= (/) )
49 47 48 eqnetrd 
 |-  ( ( ( w i^i v ) =/= (/) /\ ( w = B /\ v = [_ z / x ]_ B ) ) -> ( B i^i [_ z / x ]_ B ) =/= (/) )
50 49 adantll 
 |-  ( ( ( w =/= v /\ ( w i^i v ) =/= (/) ) /\ ( w = B /\ v = [_ z / x ]_ B ) ) -> ( B i^i [_ z / x ]_ B ) =/= (/) )
51 42 50 jca 
 |-  ( ( ( w =/= v /\ ( w i^i v ) =/= (/) ) /\ ( w = B /\ v = [_ z / x ]_ B ) ) -> ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) )
52 51 ex 
 |-  ( ( w =/= v /\ ( w i^i v ) =/= (/) ) -> ( ( w = B /\ v = [_ z / x ]_ B ) -> ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
53 52 adantl 
 |-  ( ( ( w e. ran F /\ v e. ran F ) /\ ( w =/= v /\ ( w i^i v ) =/= (/) ) ) -> ( ( w = B /\ v = [_ z / x ]_ B ) -> ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
54 53 reximdv 
 |-  ( ( ( w e. ran F /\ v e. ran F ) /\ ( w =/= v /\ ( w i^i v ) =/= (/) ) ) -> ( E. z e. A ( w = B /\ v = [_ z / x ]_ B ) -> E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
55 54 a1d 
 |-  ( ( ( w e. ran F /\ v e. ran F ) /\ ( w =/= v /\ ( w i^i v ) =/= (/) ) ) -> ( x e. A -> ( E. z e. A ( w = B /\ v = [_ z / x ]_ B ) -> E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) ) )
56 30 55 reximdai 
 |-  ( ( ( w e. ran F /\ v e. ran F ) /\ ( w =/= v /\ ( w i^i v ) =/= (/) ) ) -> ( E. x e. A E. z e. A ( w = B /\ v = [_ z / x ]_ B ) -> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
57 22 56 mpd 
 |-  ( ( ( w e. ran F /\ v e. ran F ) /\ ( w =/= v /\ ( w i^i v ) =/= (/) ) ) -> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) )
58 57 ex 
 |-  ( ( w e. ran F /\ v e. ran F ) -> ( ( w =/= v /\ ( w i^i v ) =/= (/) ) -> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
59 58 a1i 
 |-  ( -. Disj_ y e. ran F y -> ( ( w e. ran F /\ v e. ran F ) -> ( ( w =/= v /\ ( w i^i v ) =/= (/) ) -> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) ) )
60 59 rexlimdvv 
 |-  ( -. Disj_ y e. ran F y -> ( E. w e. ran F E. v e. ran F ( w =/= v /\ ( w i^i v ) =/= (/) ) -> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
61 7 60 mpd 
 |-  ( -. Disj_ y e. ran F y -> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) )
62 csbeq1 
 |-  ( u = z -> [_ u / x ]_ B = [_ z / x ]_ B )
63 62 ndisj2 
 |-  ( -. Disj_ u e. A [_ u / x ]_ B <-> E. u e. A E. z e. A ( u =/= z /\ ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/) ) )
64 nfcv 
 |-  F/_ x A
65 nfv 
 |-  F/ x u =/= z
66 nfcsb1v 
 |-  F/_ x [_ u / x ]_ B
67 66 11 nfin 
 |-  F/_ x ( [_ u / x ]_ B i^i [_ z / x ]_ B )
68 nfcv 
 |-  F/_ x (/)
69 67 68 nfne 
 |-  F/ x ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/)
70 65 69 nfan 
 |-  F/ x ( u =/= z /\ ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/) )
71 64 70 nfrex 
 |-  F/ x E. z e. A ( u =/= z /\ ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/) )
72 nfv 
 |-  F/ u E. z e. A ( x =/= z /\ ( B i^i [_ 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 i^i [_ z / x ]_ B ) = ( B i^i [_ z / x ]_ B ) )
78 77 neeq1d 
 |-  ( u = x -> ( ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/) <-> ( B i^i [_ z / x ]_ B ) =/= (/) ) )
79 73 78 anbi12d 
 |-  ( u = x -> ( ( u =/= z /\ ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/) ) <-> ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
80 79 rexbidv 
 |-  ( u = x -> ( E. z e. A ( u =/= z /\ ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/) ) <-> E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) ) )
81 71 72 80 cbvrexw 
 |-  ( E. u e. A E. z e. A ( u =/= z /\ ( [_ u / x ]_ B i^i [_ z / x ]_ B ) =/= (/) ) <-> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) )
82 63 81 bitri 
 |-  ( -. Disj_ u e. A [_ u / x ]_ B <-> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) )
83 nfcv 
 |-  F/_ u B
84 csbeq1a 
 |-  ( x = u -> B = [_ u / x ]_ B )
85 83 66 84 cbvdisj 
 |-  ( Disj_ x e. A B <-> Disj_ u e. A [_ u / x ]_ B )
86 82 85 xchnxbir 
 |-  ( -. Disj_ x e. A B <-> E. x e. A E. z e. A ( x =/= z /\ ( B i^i [_ z / x ]_ B ) =/= (/) ) )
87 61 86 sylibr 
 |-  ( -. Disj_ y e. ran F y -> -. Disj_ x e. A B )
88 87 con4i 
 |-  ( Disj_ x e. A B -> Disj_ y e. ran F y )