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 45131
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 5126 . . . . 5 (Disj 𝑦 ∈ ran 𝐹 𝑦Disj 𝑤 ∈ ran 𝐹 𝑤)
3 id 22 . . . . . . 7 (𝑤 = 𝑣𝑤 = 𝑣)
43ndisj2 44991 . . . . . 6 Disj 𝑤 ∈ ran 𝐹 𝑤 ↔ ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
54biimpi 216 . . . . 5 Disj 𝑤 ∈ ran 𝐹 𝑤 → ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
62, 5sylnbi 330 . . . 4 Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
7 disjrnmpt2.1 . . . . . . . . . . . . 13 𝐹 = (𝑥𝐴𝐵)
87elrnmpt 5972 . . . . . . . . . . . 12 (𝑤 ∈ ran 𝐹 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑥𝐴 𝑤 = 𝐵))
98ibi 267 . . . . . . . . . . 11 (𝑤 ∈ ran 𝐹 → ∃𝑥𝐴 𝑤 = 𝐵)
10 nfcv 2903 . . . . . . . . . . . . . . 15 𝑧𝐵
11 nfcsb1v 3933 . . . . . . . . . . . . . . 15 𝑥𝑧 / 𝑥𝐵
12 csbeq1a 3922 . . . . . . . . . . . . . . 15 (𝑥 = 𝑧𝐵 = 𝑧 / 𝑥𝐵)
1310, 11, 12cbvmpt 5259 . . . . . . . . . . . . . 14 (𝑥𝐴𝐵) = (𝑧𝐴𝑧 / 𝑥𝐵)
147, 13eqtri 2763 . . . . . . . . . . . . 13 𝐹 = (𝑧𝐴𝑧 / 𝑥𝐵)
1514elrnmpt 5972 . . . . . . . . . . . 12 (𝑣 ∈ ran 𝐹 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
1615ibi 267 . . . . . . . . . . 11 (𝑣 ∈ ran 𝐹 → ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵)
179, 16anim12i 613 . . . . . . . . . 10 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
18 nfv 1912 . . . . . . . . . . 11 𝑧 𝑤 = 𝐵
1911nfeq2 2921 . . . . . . . . . . 11 𝑥 𝑣 = 𝑧 / 𝑥𝐵
2018, 19reean 3314 . . . . . . . . . 10 (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ↔ (∃𝑥𝐴 𝑤 = 𝐵 ∧ ∃𝑧𝐴 𝑣 = 𝑧 / 𝑥𝐵))
2117, 20sylibr 234 . . . . . . . . 9 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
2221adantr 480 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵))
23 nfmpt1 5256 . . . . . . . . . . . . . 14 𝑥(𝑥𝐴𝐵)
247, 23nfcxfr 2901 . . . . . . . . . . . . 13 𝑥𝐹
2524nfrn 5966 . . . . . . . . . . . 12 𝑥ran 𝐹
2625nfcri 2895 . . . . . . . . . . 11 𝑥 𝑤 ∈ ran 𝐹
2725nfcri 2895 . . . . . . . . . . 11 𝑥 𝑣 ∈ ran 𝐹
2826, 27nfan 1897 . . . . . . . . . 10 𝑥(𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹)
29 nfv 1912 . . . . . . . . . 10 𝑥(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)
3028, 29nfan 1897 . . . . . . . . 9 𝑥((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅))
31 simpll 767 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝐵)
3212adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝐵 = 𝑧 / 𝑥𝐵)
33 id 22 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = 𝑧 / 𝑥𝐵𝑣 = 𝑧 / 𝑥𝐵)
3433eqcomd 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑧 / 𝑥𝐵𝑧 / 𝑥𝐵 = 𝑣)
3534ad2antlr 727 . . . . . . . . . . . . . . . . . . 19 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑧 / 𝑥𝐵 = 𝑣)
3631, 32, 353eqtrd 2779 . . . . . . . . . . . . . . . . . 18 (((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
3736adantll 714 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤 = 𝑣)
38 simpll 767 . . . . . . . . . . . . . . . . . 18 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → 𝑤𝑣)
3938neneqd 2943 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) ∧ 𝑥 = 𝑧) → ¬ 𝑤 = 𝑣)
4037, 39pm2.65da 817 . . . . . . . . . . . . . . . 16 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → ¬ 𝑥 = 𝑧)
4140neqned 2945 . . . . . . . . . . . . . . 15 ((𝑤𝑣 ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
4241adantlr 715 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑥𝑧)
43 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝐵𝑤 = 𝐵)
4443eqcomd 2741 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝐵𝐵 = 𝑤)
4544ad2antrl 728 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝐵 = 𝑤)
4634ad2antll 729 . . . . . . . . . . . . . . . . 17 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → 𝑧 / 𝑥𝐵 = 𝑣)
4745, 46ineq12d 4229 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) = (𝑤𝑣))
48 simpl 482 . . . . . . . . . . . . . . . 16 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑤𝑣) ≠ ∅)
4947, 48eqnetrd 3006 . . . . . . . . . . . . . . 15 (((𝑤𝑣) ≠ ∅ ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5049adantll 714 . . . . . . . . . . . . . 14 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
5142, 50jca 511 . . . . . . . . . . . . 13 (((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) ∧ (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵)) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5251ex 412 . . . . . . . . . . . 12 ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5352adantl 481 . . . . . . . . . . 11 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ((𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5453reximdv 3168 . . . . . . . . . 10 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5554a1d 25 . . . . . . . . 9 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (𝑥𝐴 → (∃𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
5630, 55reximdai 3259 . . . . . . . 8 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → (∃𝑥𝐴𝑧𝐴 (𝑤 = 𝐵𝑣 = 𝑧 / 𝑥𝐵) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5722, 56mpd 15 . . . . . . 7 (((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) ∧ (𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅)) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
5857ex 412 . . . . . 6 ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
5958a1i 11 . . . . 5 Disj 𝑦 ∈ ran 𝐹 𝑦 → ((𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹) → ((𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))))
6059rexlimdvv 3210 . . . 4 Disj 𝑦 ∈ ran 𝐹 𝑦 → (∃𝑤 ∈ ran 𝐹𝑣 ∈ ran 𝐹(𝑤𝑣 ∧ (𝑤𝑣) ≠ ∅) → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
616, 60mpd 15 . . 3 Disj 𝑦 ∈ ran 𝐹 𝑦 → ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
62 csbeq1 3911 . . . . . 6 (𝑢 = 𝑧𝑢 / 𝑥𝐵 = 𝑧 / 𝑥𝐵)
6362ndisj2 44991 . . . . 5 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅))
64 nfcv 2903 . . . . . . 7 𝑥𝐴
65 nfv 1912 . . . . . . . 8 𝑥 𝑢𝑧
66 nfcsb1v 3933 . . . . . . . . . 10 𝑥𝑢 / 𝑥𝐵
6766, 11nfin 4232 . . . . . . . . 9 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵)
68 nfcv 2903 . . . . . . . . 9 𝑥
6967, 68nfne 3041 . . . . . . . 8 𝑥(𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅
7065, 69nfan 1897 . . . . . . 7 𝑥(𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
7164, 70nfrexw 3311 . . . . . 6 𝑥𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅)
72 nfv 1912 . . . . . 6 𝑢𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)
73 neeq1 3001 . . . . . . . 8 (𝑢 = 𝑥 → (𝑢𝑧𝑥𝑧))
74 csbeq1 3911 . . . . . . . . . . 11 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝑥 / 𝑥𝐵)
75 csbid 3921 . . . . . . . . . . 11 𝑥 / 𝑥𝐵 = 𝐵
7674, 75eqtrdi 2791 . . . . . . . . . 10 (𝑢 = 𝑥𝑢 / 𝑥𝐵 = 𝐵)
7776ineq1d 4227 . . . . . . . . 9 (𝑢 = 𝑥 → (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) = (𝐵𝑧 / 𝑥𝐵))
7877neeq1d 2998 . . . . . . . 8 (𝑢 = 𝑥 → ((𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅ ↔ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
7973, 78anbi12d 632 . . . . . . 7 (𝑢 = 𝑥 → ((𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8079rexbidv 3177 . . . . . 6 (𝑢 = 𝑥 → (∃𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅)))
8171, 72, 80cbvrexw 3305 . . . . 5 (∃𝑢𝐴𝑧𝐴 (𝑢𝑧 ∧ (𝑢 / 𝑥𝐵𝑧 / 𝑥𝐵) ≠ ∅) ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
8263, 81bitri 275 . . . 4 Disj 𝑢𝐴 𝑢 / 𝑥𝐵 ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
83 nfcv 2903 . . . . 5 𝑢𝐵
84 csbeq1a 3922 . . . . 5 (𝑥 = 𝑢𝐵 = 𝑢 / 𝑥𝐵)
8583, 66, 84cbvdisj 5125 . . . 4 (Disj 𝑥𝐴 𝐵Disj 𝑢𝐴 𝑢 / 𝑥𝐵)
8682, 85xchnxbir 333 . . 3 Disj 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴𝑧𝐴 (𝑥𝑧 ∧ (𝐵𝑧 / 𝑥𝐵) ≠ ∅))
8761, 86sylibr 234 . 2 Disj 𝑦 ∈ ran 𝐹 𝑦 → ¬ Disj 𝑥𝐴 𝐵)
8887con4i 114 1 (Disj 𝑥𝐴 𝐵Disj 𝑦 ∈ ran 𝐹 𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1537  wcel 2106  wne 2938  wrex 3068  csb 3908  cin 3962  c0 4339  Disj wdisj 5115  cmpt 5231  ran crn 5690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-cnv 5697  df-dm 5699  df-rn 5700
This theorem is referenced by:  meadjiun  46422
  Copyright terms: Public domain W3C validator