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 )