Metamath Proof Explorer

Theorem metnrmlem3

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 5-Sep-2015)

Ref Expression
Hypotheses metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
metnrmlem.1 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
metnrmlem.2 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.3 ⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.4 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
metnrmlem.u ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) )
metnrmlem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑇 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metnrmlem.v ⊢ 𝑉 = ∪ 𝑠 ∈ 𝑆 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) )
Assertion metnrmlem3 ( 𝜑 → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 metnrmlem.1 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 metnrmlem.2 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
5 metnrmlem.3 ⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
6 metnrmlem.4 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
7 metnrmlem.u ⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) )
8 metnrmlem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑇 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
9 metnrmlem.v ⊢ 𝑉 = ∪ 𝑠 ∈ 𝑆 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) )
10 incom ⊢ ( 𝑇 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑇 )
11 10 6 syl5eq ⊢ ( 𝜑 → ( 𝑇 ∩ 𝑆 ) = ∅ )
12 8 2 3 5 4 11 9 metnrmlem2 ⊢ ( 𝜑 → ( 𝑉 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑉 ) )
13 12 simpld ⊢ ( 𝜑 → 𝑉 ∈ 𝐽 )
14 1 2 3 4 5 6 7 metnrmlem2 ⊢ ( 𝜑 → ( 𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈 ) )
15 14 simpld ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
16 12 simprd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑉 )
17 14 simprd ⊢ ( 𝜑 → 𝑇 ⊆ 𝑈 )
18 9 ineq1i ⊢ ( 𝑉 ∩ 𝑈 ) = ( ∪ 𝑠 ∈ 𝑆 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 )
19 iunin1 ⊢ ∪ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) = ( ∪ 𝑠 ∈ 𝑆 ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 )
20 18 19 eqtr4i ⊢ ( 𝑉 ∩ 𝑈 ) = ∪ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 )
21 7 ineq2i ⊢ ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) = ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
22 iunin2 ⊢ ∪ 𝑡 ∈ 𝑇 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) = ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ∪ 𝑡 ∈ 𝑇 ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
23 21 22 eqtr4i ⊢ ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) = ∪ 𝑡 ∈ 𝑇 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
24 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
25 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
26 25 cldss ⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 )
27 4 26 syl ⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
28 2 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
29 3 28 syl ⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
30 27 29 sseqtrrd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
31 30 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → 𝑠 ∈ 𝑋 )
32 31 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → 𝑠 ∈ 𝑋 )
33 25 cldss ⊢ ( 𝑇 ∈ ( Clsd ‘ 𝐽 ) → 𝑇 ⊆ ∪ 𝐽 )
34 5 33 syl ⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
35 34 29 sseqtrrd ⊢ ( 𝜑 → 𝑇 ⊆ 𝑋 )
36 35 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝑡 ∈ 𝑋 )
37 36 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → 𝑡 ∈ 𝑋 )
38 8 2 3 5 4 11 metnrmlem1a ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( 0 < ( 𝐺 ‘ 𝑠 ) ∧ if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ∈ ℝ+ ) )
39 38 simprd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ∈ ℝ+ )
40 39 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ∈ ℝ+ )
41 40 rphalfcld ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ∈ ℝ+ )
42 41 rpxrd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ∈ ℝ* )
43 1 2 3 4 5 6 metnrmlem1a ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 0 < ( 𝐹 ‘ 𝑡 ) ∧ if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ+ ) )
44 43 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 0 < ( 𝐹 ‘ 𝑡 ) ∧ if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ+ ) )
45 44 simprd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ+ )
46 45 rphalfcld ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ+ )
47 46 rpxrd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ* )
48 40 rpred ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ∈ ℝ )
49 48 rehalfcld ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ∈ ℝ )
50 45 rpred ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
51 50 rehalfcld ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ )
52 49 51 rexaddd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) +𝑒 ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) = ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) + ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
53 48 recnd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ∈ ℂ )
54 50 recnd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℂ )
55 2cnd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → 2 ∈ ℂ )
56 2ne0 ⊢ 2 ≠ 0
57 56 a1i ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → 2 ≠ 0 )
58 53 54 55 57 divdird ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) = ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) + ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) )
59 52 58 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) +𝑒 ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) = ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) )
60 8 2 3 5 4 11 metnrmlem1 ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑠 ∈ 𝑆 ) ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ≤ ( 𝑡 𝐷 𝑠 ) )
61 60 ancom2s ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ≤ ( 𝑡 𝐷 𝑠 ) )
62 xmetsym ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑡 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋 ) → ( 𝑡 𝐷 𝑠 ) = ( 𝑠 𝐷 𝑡 ) )
63 24 37 32 62 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 𝑡 𝐷 𝑠 ) = ( 𝑠 𝐷 𝑡 ) )
64 61 63 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ≤ ( 𝑠 𝐷 𝑡 ) )
65 1 2 3 4 5 6 metnrmlem1 ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ≤ ( 𝑠 𝐷 𝑡 ) )
66 40 rpxrd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ∈ ℝ* )
67 45 rpxrd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ* )
68 xmetcl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑠 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋 ) → ( 𝑠 𝐷 𝑡 ) ∈ ℝ* )
69 24 32 37 68 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 𝑠 𝐷 𝑡 ) ∈ ℝ* )
70 xle2add ⊢ ( ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ∈ ℝ* ∧ if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ* ) ∧ ( ( 𝑠 𝐷 𝑡 ) ∈ ℝ* ∧ ( 𝑠 𝐷 𝑡 ) ∈ ℝ* ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ≤ ( 𝑠 𝐷 𝑡 ) ∧ if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ≤ ( 𝑠 𝐷 𝑡 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) +𝑒 if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( 𝑠 𝐷 𝑡 ) +𝑒 ( 𝑠 𝐷 𝑡 ) ) ) )
71 66 67 69 69 70 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) ≤ ( 𝑠 𝐷 𝑡 ) ∧ if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ≤ ( 𝑠 𝐷 𝑡 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) +𝑒 if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( 𝑠 𝐷 𝑡 ) +𝑒 ( 𝑠 𝐷 𝑡 ) ) ) )
72 64 65 71 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) +𝑒 if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) ≤ ( ( 𝑠 𝐷 𝑡 ) +𝑒 ( 𝑠 𝐷 𝑡 ) ) )
73 48 50 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℝ )
74 73 recnd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) ∈ ℂ )
75 74 55 57 divcan2d ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 2 · ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) = ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) )
76 2re ⊢ 2 ∈ ℝ
77 73 rehalfcld ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ∈ ℝ )
78 rexmul ⊢ ( ( 2 ∈ ℝ ∧ ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ∈ ℝ ) → ( 2 ·e ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) = ( 2 · ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) )
79 76 77 78 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 2 ·e ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) = ( 2 · ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) )
80 48 50 rexaddd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) +𝑒 if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) = ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) )
81 75 79 80 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 2 ·e ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) = ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) +𝑒 if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) )
82 x2times ⊢ ( ( 𝑠 𝐷 𝑡 ) ∈ ℝ* → ( 2 ·e ( 𝑠 𝐷 𝑡 ) ) = ( ( 𝑠 𝐷 𝑡 ) +𝑒 ( 𝑠 𝐷 𝑡 ) ) )
83 69 82 syl ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 2 ·e ( 𝑠 𝐷 𝑡 ) ) = ( ( 𝑠 𝐷 𝑡 ) +𝑒 ( 𝑠 𝐷 𝑡 ) ) )
84 72 81 83 3brtr4d ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( 2 ·e ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) ≤ ( 2 ·e ( 𝑠 𝐷 𝑡 ) ) )
85 77 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ∈ ℝ* )
86 2rp ⊢ 2 ∈ ℝ+
87 86 a1i ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → 2 ∈ ℝ+ )
88 xlemul2 ⊢ ( ( ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ∈ ℝ* ∧ ( 𝑠 𝐷 𝑡 ) ∈ ℝ* ∧ 2 ∈ ℝ+ ) → ( ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ≤ ( 𝑠 𝐷 𝑡 ) ↔ ( 2 ·e ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) ≤ ( 2 ·e ( 𝑠 𝐷 𝑡 ) ) ) )
89 85 69 87 88 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ≤ ( 𝑠 𝐷 𝑡 ) ↔ ( 2 ·e ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ) ≤ ( 2 ·e ( 𝑠 𝐷 𝑡 ) ) ) )
90 84 89 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) + if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) ) / 2 ) ≤ ( 𝑠 𝐷 𝑡 ) )
91 59 90 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) +𝑒 ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ≤ ( 𝑠 𝐷 𝑡 ) )
92 bldisj ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑠 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋 ) ∧ ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ∈ ℝ* ∧ ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ∈ ℝ* ∧ ( ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) +𝑒 ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ≤ ( 𝑠 𝐷 𝑡 ) ) ) → ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) = ∅ )
93 24 32 37 42 47 91 92 syl33anc ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) = ∅ )
94 eqimss ⊢ ( ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) = ∅ → ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) ⊆ ∅ )
95 93 94 syl ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇 ) ) → ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) ⊆ ∅ )
96 95 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) ∧ 𝑡 ∈ 𝑇 ) → ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) ⊆ ∅ )
97 96 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ∀ 𝑡 ∈ 𝑇 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) ⊆ ∅ )
98 iunss ⊢ ( ∪ 𝑡 ∈ 𝑇 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) ⊆ ∅ ↔ ∀ 𝑡 ∈ 𝑇 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) ⊆ ∅ )
99 97 98 sylibr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ∪ 𝑡 ∈ 𝑇 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ ( 𝑡 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐹 ‘ 𝑡 ) , 1 , ( 𝐹 ‘ 𝑡 ) ) / 2 ) ) ) ⊆ ∅ )
100 23 99 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) ⊆ ∅ )
101 100 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) ⊆ ∅ )
102 iunss ⊢ ( ∪ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) ⊆ ∅ ↔ ∀ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) ⊆ ∅ )
103 101 102 sylibr ⊢ ( 𝜑 → ∪ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) ⊆ ∅ )
104 ss0 ⊢ ( ∪ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) ⊆ ∅ → ∪ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) = ∅ )
105 103 104 syl ⊢ ( 𝜑 → ∪ 𝑠 ∈ 𝑆 ( ( 𝑠 ( ball ‘ 𝐷 ) ( if ( 1 ≤ ( 𝐺 ‘ 𝑠 ) , 1 , ( 𝐺 ‘ 𝑠 ) ) / 2 ) ) ∩ 𝑈 ) = ∅ )
106 20 105 syl5eq ⊢ ( 𝜑 → ( 𝑉 ∩ 𝑈 ) = ∅ )
107 sseq2 ⊢ ( 𝑧 = 𝑉 → ( 𝑆 ⊆ 𝑧 ↔ 𝑆 ⊆ 𝑉 ) )
108 ineq1 ⊢ ( 𝑧 = 𝑉 → ( 𝑧 ∩ 𝑤 ) = ( 𝑉 ∩ 𝑤 ) )
109 108 eqeq1d ⊢ ( 𝑧 = 𝑉 → ( ( 𝑧 ∩ 𝑤 ) = ∅ ↔ ( 𝑉 ∩ 𝑤 ) = ∅ ) )
110 107 109 3anbi13d ⊢ ( 𝑧 = 𝑉 → ( ( 𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑤 ∧ ( 𝑉 ∩ 𝑤 ) = ∅ ) ) )
111 sseq2 ⊢ ( 𝑤 = 𝑈 → ( 𝑇 ⊆ 𝑤 ↔ 𝑇 ⊆ 𝑈 ) )
112 ineq2 ⊢ ( 𝑤 = 𝑈 → ( 𝑉 ∩ 𝑤 ) = ( 𝑉 ∩ 𝑈 ) )
113 112 eqeq1d ⊢ ( 𝑤 = 𝑈 → ( ( 𝑉 ∩ 𝑤 ) = ∅ ↔ ( 𝑉 ∩ 𝑈 ) = ∅ ) )
114 111 113 3anbi23d ⊢ ( 𝑤 = 𝑈 → ( ( 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑤 ∧ ( 𝑉 ∩ 𝑤 ) = ∅ ) ↔ ( 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈 ∧ ( 𝑉 ∩ 𝑈 ) = ∅ ) ) )
115 110 114 rspc2ev ⊢ ( ( 𝑉 ∈ 𝐽 ∧ 𝑈 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈 ∧ ( 𝑉 ∩ 𝑈 ) = ∅ ) ) → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )
116 13 15 16 17 106 115 syl113anc ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )