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

Theorem disjrnmpt2 43886
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 5125 . . . . 5 (Disj 𝑦 ∈ ran 𝐹 𝑦Disj 𝑤 ∈ ran 𝐹 𝑤)
3 id 22 . . . . . . 7 (𝑤 = 𝑣𝑤 = 𝑣)
43ndisj2 43738 . . . . . 6 Disj 𝑤 ∈ ran 𝐹 𝑤 ↔ ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
54biimpi 215 . . . . 5 Disj 𝑤 ∈ ran 𝐹 𝑤 → ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
62, 5sylnbi 330 . . . 4 Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
7 disjrnmpt2.1 . . . . . . . . . . . . 13 𝐹 = (𝑥𝐴𝐵)
87elrnmpt 5956 . . . . . . . . . . . 12 (𝑤 ∈ ran 𝐹 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝑤 = 𝐵))
98ibi 267 . . . . . . . . . . 11 (𝑤 ∈ ran 𝐹 → ∃𝑥𝐴 𝑤 = 𝐵)
10 nfcv 2904 . . . . . . . . . . . . . . 15 𝑧𝐵
11 nfcsb1v 3919 . . . . . . . . . . . . . . 15 𝑥𝑧 / 𝑥𝐵
12 csbeq1a 3908 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
1310, 11, 12cbvmpt 5260 . . . . . . . . . . . . . 14 (𝑥𝐴𝐵) = (𝑧𝐴𝑧 / 𝑥𝐵)
147, 13eqtri 2761 . . . . . . . . . . . . 13 𝐹 = (𝑧𝐴𝑧 / 𝑥𝐵)
1514elrnmpt 5956 . . . . . . . . . . . 12 (𝑣 ∈ ran 𝐹 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
1615ibi 267 . . . . . . . . . . 11 (𝑣 ∈ ran 𝐹 → ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵)
179, 16anim12i 614 . . . . . . . . . 10 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
18 nfv 1918 . . . . . . . . . . 11 𝑧 𝑤 = 𝐵
1911nfeq2 2921 . . . . . . . . . . 11 𝑥 𝑣 = 𝑧 / 𝑥𝐵
2018, 19reean 3314 . . . . . . . . . 10 (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ↔ (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
2117, 20sylibr 233 . . . . . . . . 9 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
2221adantr 482 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
23 nfmpt1 5257 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴𝐵)
247, 23nfcxfr 2902 . . . . . . . . . . . . 13 𝑥𝐹
2524nfrn 5952 . . . . . . . . . . . 12 𝑥ran 𝐹
2625nfcri 2891 . . . . . . . . . . 11 𝑥 𝑤 ∈ ran 𝐹
2725nfcri 2891 . . . . . . . . . . 11 𝑥 𝑣 ∈ ran 𝐹
2826, 27nfan 1903 . . . . . . . . . 10 𝑥(𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹)
29 nfv 1918 . . . . . . . . . 10 𝑥(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)
3028, 29nfan 1903 . . . . . . . . 9 𝑥((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
31 simpll 766 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝐵)
3212adantl 483 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝐵 = 𝑧 / 𝑥𝐵)
33 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑧 / 𝑥𝐵𝑣 = 𝑧 / 𝑥𝐵)
3433eqcomd 2739 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑧 / 𝑥𝐵𝑧 / 𝑥𝐵 = 𝑣)
3534ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑧 / 𝑥𝐵 = 𝑣)
3631, 32, 353eqtrd 2777 . . . . . . . . . . . . . . . . . 18 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
3736adantll 713 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
38 simpll 766 . . . . . . . . . . . . . . . . . 18 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤𝑣)
3938neneqd 2946 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → ¬ 𝑤 = 𝑣)
4037, 39pm2.65da 816 . . . . . . . . . . . . . . . 16 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → ¬ 𝑥 = 𝑧)
4140neqned 2948 . . . . . . . . . . . . . . 15 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
4241adantlr 714 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
43 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝐵𝑤 = 𝐵)
4443eqcomd 2739 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝐵𝐵 = 𝑤)
4544ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝐵 = 𝑤)
4634ad2antll 728 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥𝐵 = 𝑣)
4745, 46ineq12d 4214 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) = (𝑤𝑣))
48 simpl 484 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑤𝑣) ≠ ∅)
4947, 48eqnetrd 3009 . . . . . . . . . . . . . . 15 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5049adantll 713 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5142, 50jca 513 . . . . . . . . . . . . 13 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5251ex 414 . . . . . . . . . . . 12 ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5352adantl 483 . . . . . . . . . . 11 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5453reximdv 3171 . . . . . . . . . 10 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5554a1d 25 . . . . . . . . 9 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (𝑥𝐴 → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
5630, 55reximdai 3259 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5722, 56mpd 15 . . . . . . 7 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5857ex 414 . . . . . 6 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5958a1i 11 . . . . 5 Disj 𝑦 ∈ ran 𝐹 𝑦 → ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
6059rexlimdvv 3211 . . . 4 Disj 𝑦 ∈ ran 𝐹 𝑦 → (∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
616, 60mpd 15 . . 3 Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
62 csbeq1 3897 . . . . . 6 (𝑢 = 𝑧𝑢 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
6362ndisj2 43738 . . . . 5 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅))
64 nfcv 2904 . . . . . . 7 𝑥𝐴
65 nfv 1918 . . . . . . . 8 𝑥 𝑢𝑧
66 nfcsb1v 3919 . . . . . . . . . 10 𝑥𝑢 / 𝑥𝐵
6766, 11nfin 4217 . . . . . . . . 9 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵)
68 nfcv 2904 . . . . . . . . 9 𝑥
6967, 68nfne 3044 . . . . . . . 8 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅
7065, 69nfan 1903 . . . . . . 7 𝑥(𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
7164, 70nfrexw 3311 . . . . . 6 𝑥𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
72 nfv 1918 . . . . . 6 𝑢𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
73 neeq1 3004 . . . . . . . 8 (𝑢 = 𝑥 → (𝑢𝑧𝑥𝑧))
74 csbeq1 3897 . . . . . . . . . . 11 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝑥 / 𝑥𝐵)
75 csbid 3907 . . . . . . . . . . 11 𝑥 / 𝑥𝐵 = 𝐵
7674, 75eqtrdi 2789 . . . . . . . . . 10 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝐵)
7776ineq1d 4212 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) = (𝐵𝑧 / 𝑥𝐵))
7877neeq1d 3001 . . . . . . . 8 (𝑢 = 𝑥 → ((𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅ ↔ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
7973, 78anbi12d 632 . . . . . . 7 (𝑢 = 𝑥 → ((𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8079rexbidv 3179 . . . . . 6 (𝑢 = 𝑥 → (∃𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8171, 72, 80cbvrexw 3305 . . . . 5 (∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
8263, 81bitri 275 . . . 4 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
83 nfcv 2904 . . . . 5 𝑢𝐵
84 csbeq1a 3908 . . . . 5 (𝑥 = 𝑢𝐵 = 𝑢 / 𝑥𝐵)
8583, 66, 84cbvdisj 5124 . . . 4 (Disj 𝑥𝐴 𝐵Disj 𝑢𝐴 𝑢 / 𝑥𝐵)
8682, 85xchnxbir 333 . . 3 Disj 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
8761, 86sylibr 233 . 2 Disj 𝑦 ∈ ran 𝐹 𝑦 → ¬ Disj 𝑥𝐴 𝐵)
8887con4i 114 1 (Disj 𝑥𝐴 𝐵Disj 𝑦 ∈ ran 𝐹 𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wcel 2107  wne 2941  wrex 3071  csb 3894  cin 3948  c0 4323  Disj wdisj 5114  cmpt 5232  ran crn 5678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-disj 5115  df-br 5150  df-opab 5212  df-mpt 5233  df-cnv 5685  df-dm 5687  df-rn 5688
This theorem is referenced by:  meadjiun  45182
  Copyright terms: Public domain W3C validator