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 𝐹 = ( 𝑥𝐴𝐵 )
Assertion disjrnmpt2 ( Disj 𝑥𝐴 𝐵Disj 𝑦 ∈ ran 𝐹 𝑦 )

Proof

Step Hyp Ref Expression
1 disjrnmpt2.1 𝐹 = ( 𝑥𝐴𝐵 )
2 id ( 𝑦 = 𝑤𝑦 = 𝑤 )
3 2 cbvdisjv ( Disj 𝑦 ∈ ran 𝐹 𝑦Disj 𝑤 ∈ ran 𝐹 𝑤 )
4 id ( 𝑤 = 𝑣𝑤 = 𝑣 )
5 4 ndisj2 ( ¬ Disj 𝑤 ∈ ran 𝐹 𝑤 ↔ ∃ 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) )
6 5 biimpi ( ¬ Disj 𝑤 ∈ ran 𝐹 𝑤 → ∃ 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) )
7 3 6 sylnbi ( ¬ Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃ 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) )
8 1 elrnmpt ( 𝑤 ∈ ran 𝐹 → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑥𝐴 𝑤 = 𝐵 ) )
9 8 ibi ( 𝑤 ∈ ran 𝐹 → ∃ 𝑥𝐴 𝑤 = 𝐵 )
10 nfcv 𝑧 𝐵
11 nfcsb1v 𝑥 𝑧 / 𝑥 𝐵
12 csbeq1a ( 𝑥 = 𝑧𝐵 = 𝑧 / 𝑥 𝐵 )
13 10 11 12 cbvmpt ( 𝑥𝐴𝐵 ) = ( 𝑧𝐴 𝑧 / 𝑥 𝐵 )
14 1 13 eqtri 𝐹 = ( 𝑧𝐴 𝑧 / 𝑥 𝐵 )
15 14 elrnmpt ( 𝑣 ∈ ran 𝐹 → ( 𝑣 ∈ ran 𝐹 ↔ ∃ 𝑧𝐴 𝑣 = 𝑧 / 𝑥 𝐵 ) )
16 15 ibi ( 𝑣 ∈ ran 𝐹 → ∃ 𝑧𝐴 𝑣 = 𝑧 / 𝑥 𝐵 )
17 9 16 anim12i ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) → ( ∃ 𝑥𝐴 𝑤 = 𝐵 ∧ ∃ 𝑧𝐴 𝑣 = 𝑧 / 𝑥 𝐵 ) )
18 nfv 𝑧 𝑤 = 𝐵
19 11 nfeq2 𝑥 𝑣 = 𝑧 / 𝑥 𝐵
20 18 19 reean ( ∃ 𝑥𝐴𝑧𝐴 ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ↔ ( ∃ 𝑥𝐴 𝑤 = 𝐵 ∧ ∃ 𝑧𝐴 𝑣 = 𝑧 / 𝑥 𝐵 ) )
21 17 20 sylibr ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) → ∃ 𝑥𝐴𝑧𝐴 ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) )
22 21 adantr ( ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) ∧ ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ) → ∃ 𝑥𝐴𝑧𝐴 ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) )
23 nfmpt1 𝑥 ( 𝑥𝐴𝐵 )
24 1 23 nfcxfr 𝑥 𝐹
25 24 nfrn 𝑥 ran 𝐹
26 25 nfcri 𝑥 𝑤 ∈ ran 𝐹
27 25 nfcri 𝑥 𝑣 ∈ ran 𝐹
28 26 27 nfan 𝑥 ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 )
29 nfv 𝑥 ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ )
30 28 29 nfan 𝑥 ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) ∧ ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) )
31 simpll ( ( ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ∧ 𝑥 = 𝑧 ) → 𝑤 = 𝐵 )
32 12 adantl ( ( ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ∧ 𝑥 = 𝑧 ) → 𝐵 = 𝑧 / 𝑥 𝐵 )
33 id ( 𝑣 = 𝑧 / 𝑥 𝐵𝑣 = 𝑧 / 𝑥 𝐵 )
34 33 eqcomd ( 𝑣 = 𝑧 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 = 𝑣 )
35 34 ad2antlr ( ( ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ∧ 𝑥 = 𝑧 ) → 𝑧 / 𝑥 𝐵 = 𝑣 )
36 31 32 35 3eqtrd ( ( ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ∧ 𝑥 = 𝑧 ) → 𝑤 = 𝑣 )
37 36 adantll ( ( ( 𝑤𝑣 ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) ∧ 𝑥 = 𝑧 ) → 𝑤 = 𝑣 )
38 simpll ( ( ( 𝑤𝑣 ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) ∧ 𝑥 = 𝑧 ) → 𝑤𝑣 )
39 38 neneqd ( ( ( 𝑤𝑣 ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) ∧ 𝑥 = 𝑧 ) → ¬ 𝑤 = 𝑣 )
40 37 39 pm2.65da ( ( 𝑤𝑣 ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → ¬ 𝑥 = 𝑧 )
41 40 neqned ( ( 𝑤𝑣 ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → 𝑥𝑧 )
42 41 adantlr ( ( ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → 𝑥𝑧 )
43 id ( 𝑤 = 𝐵𝑤 = 𝐵 )
44 43 eqcomd ( 𝑤 = 𝐵𝐵 = 𝑤 )
45 44 ad2antrl ( ( ( 𝑤𝑣 ) ≠ ∅ ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → 𝐵 = 𝑤 )
46 34 ad2antll ( ( ( 𝑤𝑣 ) ≠ ∅ ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → 𝑧 / 𝑥 𝐵 = 𝑣 )
47 45 46 ineq12d ( ( ( 𝑤𝑣 ) ≠ ∅ ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → ( 𝐵 𝑧 / 𝑥 𝐵 ) = ( 𝑤𝑣 ) )
48 simpl ( ( ( 𝑤𝑣 ) ≠ ∅ ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → ( 𝑤𝑣 ) ≠ ∅ )
49 47 48 eqnetrd ( ( ( 𝑤𝑣 ) ≠ ∅ ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ )
50 49 adantll ( ( ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ )
51 42 50 jca ( ( ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ∧ ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) ) → ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
52 51 ex ( ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) → ( ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) → ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
53 52 adantl ( ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) ∧ ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ) → ( ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) → ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
54 53 reximdv ( ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) ∧ ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ) → ( ∃ 𝑧𝐴 ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) → ∃ 𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
55 54 a1d ( ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) ∧ ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ) → ( 𝑥𝐴 → ( ∃ 𝑧𝐴 ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) → ∃ 𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) ) )
56 30 55 reximdai ( ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) ∧ ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ) → ( ∃ 𝑥𝐴𝑧𝐴 ( 𝑤 = 𝐵𝑣 = 𝑧 / 𝑥 𝐵 ) → ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
57 22 56 mpd ( ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) ∧ ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) ) → ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
58 57 ex ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) → ( ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) → ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
59 58 a1i ( ¬ Disj 𝑦 ∈ ran 𝐹 𝑦 → ( ( 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ) → ( ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) → ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) ) )
60 59 rexlimdvv ( ¬ Disj 𝑦 ∈ ran 𝐹 𝑦 → ( ∃ 𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹 ( 𝑤𝑣 ∧ ( 𝑤𝑣 ) ≠ ∅ ) → ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
61 7 60 mpd ( ¬ Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
62 csbeq1 ( 𝑢 = 𝑧 𝑢 / 𝑥 𝐵 = 𝑧 / 𝑥 𝐵 )
63 62 ndisj2 ( ¬ Disj 𝑢𝐴 𝑢 / 𝑥 𝐵 ↔ ∃ 𝑢𝐴𝑧𝐴 ( 𝑢𝑧 ∧ ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
64 nfcv 𝑥 𝐴
65 nfv 𝑥 𝑢𝑧
66 nfcsb1v 𝑥 𝑢 / 𝑥 𝐵
67 66 11 nfin 𝑥 ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 )
68 nfcv 𝑥
69 67 68 nfne 𝑥 ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅
70 65 69 nfan 𝑥 ( 𝑢𝑧 ∧ ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ )
71 64 70 nfrex 𝑥𝑧𝐴 ( 𝑢𝑧 ∧ ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ )
72 nfv 𝑢𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ )
73 neeq1 ( 𝑢 = 𝑥 → ( 𝑢𝑧𝑥𝑧 ) )
74 csbeq1 ( 𝑢 = 𝑥 𝑢 / 𝑥 𝐵 = 𝑥 / 𝑥 𝐵 )
75 csbid 𝑥 / 𝑥 𝐵 = 𝐵
76 74 75 eqtrdi ( 𝑢 = 𝑥 𝑢 / 𝑥 𝐵 = 𝐵 )
77 76 ineq1d ( 𝑢 = 𝑥 → ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ( 𝐵 𝑧 / 𝑥 𝐵 ) )
78 77 neeq1d ( 𝑢 = 𝑥 → ( ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ↔ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
79 73 78 anbi12d ( 𝑢 = 𝑥 → ( ( 𝑢𝑧 ∧ ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ↔ ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
80 79 rexbidv ( 𝑢 = 𝑥 → ( ∃ 𝑧𝐴 ( 𝑢𝑧 ∧ ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ↔ ∃ 𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ) )
81 71 72 80 cbvrexw ( ∃ 𝑢𝐴𝑧𝐴 ( 𝑢𝑧 ∧ ( 𝑢 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) ↔ ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
82 63 81 bitri ( ¬ Disj 𝑢𝐴 𝑢 / 𝑥 𝐵 ↔ ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
83 nfcv 𝑢 𝐵
84 csbeq1a ( 𝑥 = 𝑢𝐵 = 𝑢 / 𝑥 𝐵 )
85 83 66 84 cbvdisj ( Disj 𝑥𝐴 𝐵Disj 𝑢𝐴 𝑢 / 𝑥 𝐵 )
86 82 85 xchnxbir ( ¬ Disj 𝑥𝐴 𝐵 ↔ ∃ 𝑥𝐴𝑧𝐴 ( 𝑥𝑧 ∧ ( 𝐵 𝑧 / 𝑥 𝐵 ) ≠ ∅ ) )
87 61 86 sylibr ( ¬ Disj 𝑦 ∈ ran 𝐹 𝑦 → ¬ Disj 𝑥𝐴 𝐵 )
88 87 con4i ( Disj 𝑥𝐴 𝐵Disj 𝑦 ∈ ran 𝐹 𝑦 )