Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  disjrnmpt2 Structured version   Visualization version   GIF version

Theorem disjrnmpt2 41310
 Description: Disjointness of the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
disjrnmpt2.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
disjrnmpt2 (Disj 𝑥𝐴 𝐵Disj 𝑦 ∈ ran 𝐹 𝑦)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐹
Allowed substitution hints:   𝐴(𝑦)   𝐵(𝑥,𝑦)   𝐹(𝑥)

Proof of Theorem disjrnmpt2
Dummy variables 𝑢 𝑧 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . . . 6 (𝑦 = 𝑤𝑦 = 𝑤)
21cbvdisjv 5038 . . . . 5 (Disj 𝑦 ∈ ran 𝐹 𝑦Disj 𝑤 ∈ ran 𝐹 𝑤)
3 id 22 . . . . . . 7 (𝑤 = 𝑣𝑤 = 𝑣)
43ndisj2 41174 . . . . . 6 Disj 𝑤 ∈ ran 𝐹 𝑤 ↔ ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
54biimpi 217 . . . . 5 Disj 𝑤 ∈ ran 𝐹 𝑤 → ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
62, 5sylnbi 331 . . . 4 Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
7 disjrnmpt2.1 . . . . . . . . . . . . 13 𝐹 = (𝑥𝐴𝐵)
87elrnmpt 5826 . . . . . . . . . . . 12 (𝑤 ∈ ran 𝐹 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝑤 = 𝐵))
98ibi 268 . . . . . . . . . . 11 (𝑤 ∈ ran 𝐹 → ∃𝑥𝐴 𝑤 = 𝐵)
10 nfcv 2981 . . . . . . . . . . . . . . 15 𝑧𝐵
11 nfcsb1v 3910 . . . . . . . . . . . . . . 15 𝑥𝑧 / 𝑥𝐵
12 csbeq1a 3900 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
1310, 11, 12cbvmpt 5163 . . . . . . . . . . . . . 14 (𝑥𝐴𝐵) = (𝑧𝐴𝑧 / 𝑥𝐵)
147, 13eqtri 2848 . . . . . . . . . . . . 13 𝐹 = (𝑧𝐴𝑧 / 𝑥𝐵)
1514elrnmpt 5826 . . . . . . . . . . . 12 (𝑣 ∈ ran 𝐹 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
1615ibi 268 . . . . . . . . . . 11 (𝑣 ∈ ran 𝐹 → ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵)
179, 16anim12i 612 . . . . . . . . . 10 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
18 nfv 1908 . . . . . . . . . . 11 𝑧 𝑤 = 𝐵
1911nfeq2 2999 . . . . . . . . . . 11 𝑥 𝑣 = 𝑧 / 𝑥𝐵
2018, 19reean 3371 . . . . . . . . . 10 (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ↔ (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
2117, 20sylibr 235 . . . . . . . . 9 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
2221adantr 481 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
23 nfmpt1 5160 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴𝐵)
247, 23nfcxfr 2979 . . . . . . . . . . . . 13 𝑥𝐹
2524nfrn 5822 . . . . . . . . . . . 12 𝑥ran 𝐹
2625nfcri 2975 . . . . . . . . . . 11 𝑥 𝑤 ∈ ran 𝐹
2725nfcri 2975 . . . . . . . . . . 11 𝑥 𝑣 ∈ ran 𝐹
2826, 27nfan 1893 . . . . . . . . . 10 𝑥(𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹)
29 nfv 1908 . . . . . . . . . 10 𝑥(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)
3028, 29nfan 1893 . . . . . . . . 9 𝑥((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
31 simpll 763 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝐵)
3212adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝐵 = 𝑧 / 𝑥𝐵)
33 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑧 / 𝑥𝐵𝑣 = 𝑧 / 𝑥𝐵)
3433eqcomd 2831 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑧 / 𝑥𝐵𝑧 / 𝑥𝐵 = 𝑣)
3534ad2antlr 723 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑧 / 𝑥𝐵 = 𝑣)
3631, 32, 353eqtrd 2864 . . . . . . . . . . . . . . . . . 18 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
3736adantll 710 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
38 simpll 763 . . . . . . . . . . . . . . . . . 18 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤𝑣)
3938neneqd 3025 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → ¬ 𝑤 = 𝑣)
4037, 39pm2.65da 813 . . . . . . . . . . . . . . . 16 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → ¬ 𝑥 = 𝑧)
4140neqned 3027 . . . . . . . . . . . . . . 15 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
4241adantlr 711 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
43 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝐵𝑤 = 𝐵)
4443eqcomd 2831 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝐵𝐵 = 𝑤)
4544ad2antrl 724 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝐵 = 𝑤)
4634ad2antll 725 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥𝐵 = 𝑣)
4745, 46ineq12d 4193 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) = (𝑤𝑣))
48 simpl 483 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑤𝑣) ≠ ∅)
4947, 48eqnetrd 3087 . . . . . . . . . . . . . . 15 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5049adantll 710 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5142, 50jca 512 . . . . . . . . . . . . 13 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5251ex 413 . . . . . . . . . . . 12 ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5352adantl 482 . . . . . . . . . . 11 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5453reximdv 3277 . . . . . . . . . 10 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5554a1d 25 . . . . . . . . 9 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (𝑥𝐴 → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
5630, 55reximdai 3315 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5722, 56mpd 15 . . . . . . 7 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5857ex 413 . . . . . 6 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5958a1i 11 . . . . 5 Disj 𝑦 ∈ ran 𝐹 𝑦 → ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
6059rexlimdvv 3297 . . . 4 Disj 𝑦 ∈ ran 𝐹 𝑦 → (∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
616, 60mpd 15 . . 3 Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
62 csbeq1 3889 . . . . . 6 (𝑢 = 𝑧𝑢 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
6362ndisj2 41174 . . . . 5 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅))
64 nfcv 2981 . . . . . . 7 𝑥𝐴
65 nfv 1908 . . . . . . . 8 𝑥 𝑢𝑧
66 nfcsb1v 3910 . . . . . . . . . 10 𝑥𝑢 / 𝑥𝐵
6766, 11nfin 4196 . . . . . . . . 9 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵)
68 nfcv 2981 . . . . . . . . 9 𝑥
6967, 68nfne 3123 . . . . . . . 8 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅
7065, 69nfan 1893 . . . . . . 7 𝑥(𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
7164, 70nfrex 3313 . . . . . 6 𝑥𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
72 nfv 1908 . . . . . 6 𝑢𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
73 neeq1 3082 . . . . . . . 8 (𝑢 = 𝑥 → (𝑢𝑧𝑥𝑧))
74 csbeq1 3889 . . . . . . . . . . 11 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝑥 / 𝑥𝐵)
75 csbid 3899 . . . . . . . . . . 11 𝑥 / 𝑥𝐵 = 𝐵
7674, 75syl6eq 2876 . . . . . . . . . 10 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝐵)
7776ineq1d 4191 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) = (𝐵𝑧 / 𝑥𝐵))
7877neeq1d 3079 . . . . . . . 8 (𝑢 = 𝑥 → ((𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅ ↔ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
7973, 78anbi12d 630 . . . . . . 7 (𝑢 = 𝑥 → ((𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8079rexbidv 3301 . . . . . 6 (𝑢 = 𝑥 → (∃𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8171, 72, 80cbvrex 3451 . . . . 5 (∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
8263, 81bitri 276 . . . 4 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
83 nfcv 2981 . . . . 5 𝑢𝐵
84 csbeq1a 3900 . . . . 5 (𝑥 = 𝑢𝐵 = 𝑢 / 𝑥𝐵)
8583, 66, 84cbvdisj 5037 . . . 4 (Disj 𝑥𝐴 𝐵Disj 𝑢𝐴 𝑢 / 𝑥𝐵)
8682, 85xchnxbir 334 . . 3 Disj 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
8761, 86sylibr 235 . 2 Disj 𝑦 ∈ ran 𝐹 𝑦 → ¬ Disj 𝑥𝐴 𝐵)
8887con4i 114 1 (Disj 𝑥𝐴 𝐵Disj 𝑦 ∈ ran 𝐹 𝑦)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1530   ∈ wcel 2107   ≠ wne 3020  ∃wrex 3143  ⦋csb 3886   ∩ cin 3938  ∅c0 4294  Disj wdisj 5027   ↦ cmpt 5142  ran crn 5554 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-sep 5199  ax-nul 5206  ax-pr 5325 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-disj 5028  df-br 5063  df-opab 5125  df-mpt 5143  df-cnv 5561  df-dm 5563  df-rn 5564 This theorem is referenced by:  meadjiun  42610
 Copyright terms: Public domain W3C validator