This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion disjrnmpt2 ( Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ ran 𝐹 𝑦 )

Proof

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