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 ⊢ F = x ∈ A ⟼ B
Assertion disjrnmpt2 ⊢ Disj x ∈ A B → Disj y ∈ ran ⁡ F y

Proof

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