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 43481
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 5086 . . . . 5 (Disj 𝑦 ∈ ran 𝐹 𝑦Disj 𝑤 ∈ ran 𝐹 𝑤)
3 id 22 . . . . . . 7 (𝑤 = 𝑣𝑤 = 𝑣)
43ndisj2 43333 . . . . . 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 5916 . . . . . . . . . . . 12 (𝑤 ∈ ran 𝐹 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝑤 = 𝐵))
98ibi 267 . . . . . . . . . . 11 (𝑤 ∈ ran 𝐹 → ∃𝑥𝐴 𝑤 = 𝐵)
10 nfcv 2908 . . . . . . . . . . . . . . 15 𝑧𝐵
11 nfcsb1v 3885 . . . . . . . . . . . . . . 15 𝑥𝑧 / 𝑥𝐵
12 csbeq1a 3874 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
1310, 11, 12cbvmpt 5221 . . . . . . . . . . . . . 14 (𝑥𝐴𝐵) = (𝑧𝐴𝑧 / 𝑥𝐵)
147, 13eqtri 2765 . . . . . . . . . . . . 13 𝐹 = (𝑧𝐴𝑧 / 𝑥𝐵)
1514elrnmpt 5916 . . . . . . . . . . . 12 (𝑣 ∈ ran 𝐹 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
1615ibi 267 . . . . . . . . . . 11 (𝑣 ∈ ran 𝐹 → ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵)
179, 16anim12i 614 . . . . . . . . . 10 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
18 nfv 1918 . . . . . . . . . . 11 𝑧 𝑤 = 𝐵
1911nfeq2 2925 . . . . . . . . . . 11 𝑥 𝑣 = 𝑧 / 𝑥𝐵
2018, 19reean 3302 . . . . . . . . . 10 (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ↔ (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
2117, 20sylibr 233 . . . . . . . . 9 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
2221adantr 482 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
23 nfmpt1 5218 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴𝐵)
247, 23nfcxfr 2906 . . . . . . . . . . . . 13 𝑥𝐹
2524nfrn 5912 . . . . . . . . . . . 12 𝑥ran 𝐹
2625nfcri 2895 . . . . . . . . . . 11 𝑥 𝑤 ∈ ran 𝐹
2725nfcri 2895 . . . . . . . . . . 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 2743 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑧 / 𝑥𝐵𝑧 / 𝑥𝐵 = 𝑣)
3534ad2antlr 726 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑧 / 𝑥𝐵 = 𝑣)
3631, 32, 353eqtrd 2781 . . . . . . . . . . . . . . . . . 18 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
3736adantll 713 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
38 simpll 766 . . . . . . . . . . . . . . . . . 18 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤𝑣)
3938neneqd 2949 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → ¬ 𝑤 = 𝑣)
4037, 39pm2.65da 816 . . . . . . . . . . . . . . . 16 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → ¬ 𝑥 = 𝑧)
4140neqned 2951 . . . . . . . . . . . . . . 15 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
4241adantlr 714 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
43 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝐵𝑤 = 𝐵)
4443eqcomd 2743 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝐵𝐵 = 𝑤)
4544ad2antrl 727 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝐵 = 𝑤)
4634ad2antll 728 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥𝐵 = 𝑣)
4745, 46ineq12d 4178 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) = (𝑤𝑣))
48 simpl 484 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑤𝑣) ≠ ∅)
4947, 48eqnetrd 3012 . . . . . . . . . . . . . . 15 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5049adantll 713 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5142, 50jca 513 . . . . . . . . . . . . 13 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5251ex 414 . . . . . . . . . . . 12 ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5352adantl 483 . . . . . . . . . . 11 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5453reximdv 3168 . . . . . . . . . 10 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5554a1d 25 . . . . . . . . 9 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (𝑥𝐴 → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
5630, 55reximdai 3247 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5722, 56mpd 15 . . . . . . 7 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5857ex 414 . . . . . 6 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5958a1i 11 . . . . 5 Disj 𝑦 ∈ ran 𝐹 𝑦 → ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
6059rexlimdvv 3205 . . . 4 Disj 𝑦 ∈ ran 𝐹 𝑦 → (∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
616, 60mpd 15 . . 3 Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
62 csbeq1 3863 . . . . . 6 (𝑢 = 𝑧𝑢 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
6362ndisj2 43333 . . . . 5 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅))
64 nfcv 2908 . . . . . . 7 𝑥𝐴
65 nfv 1918 . . . . . . . 8 𝑥 𝑢𝑧
66 nfcsb1v 3885 . . . . . . . . . 10 𝑥𝑢 / 𝑥𝐵
6766, 11nfin 4181 . . . . . . . . 9 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵)
68 nfcv 2908 . . . . . . . . 9 𝑥
6967, 68nfne 3046 . . . . . . . 8 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅
7065, 69nfan 1903 . . . . . . 7 𝑥(𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
7164, 70nfrexw 3299 . . . . . 6 𝑥𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
72 nfv 1918 . . . . . 6 𝑢𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
73 neeq1 3007 . . . . . . . 8 (𝑢 = 𝑥 → (𝑢𝑧𝑥𝑧))
74 csbeq1 3863 . . . . . . . . . . 11 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝑥 / 𝑥𝐵)
75 csbid 3873 . . . . . . . . . . 11 𝑥 / 𝑥𝐵 = 𝐵
7674, 75eqtrdi 2793 . . . . . . . . . 10 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝐵)
7776ineq1d 4176 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) = (𝐵𝑧 / 𝑥𝐵))
7877neeq1d 3004 . . . . . . . 8 (𝑢 = 𝑥 → ((𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅ ↔ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
7973, 78anbi12d 632 . . . . . . 7 (𝑢 = 𝑥 → ((𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8079rexbidv 3176 . . . . . 6 (𝑢 = 𝑥 → (∃𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8171, 72, 80cbvrexw 3293 . . . . 5 (∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
8263, 81bitri 275 . . . 4 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
83 nfcv 2908 . . . . 5 𝑢𝐵
84 csbeq1a 3874 . . . . 5 (𝑥 = 𝑢𝐵 = 𝑢 / 𝑥𝐵)
8583, 66, 84cbvdisj 5085 . . . 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 2944  wrex 3074  csb 3860  cin 3914  c0 4287  Disj wdisj 5075  cmpt 5193  ran crn 5639
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 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3356  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-cnv 5646  df-dm 5648  df-rn 5649
This theorem is referenced by:  meadjiun  44781
  Copyright terms: Public domain W3C validator