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	eqtrid	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑆 ) = ∅ )
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	eqtrid	⊢ ( 𝜑 → ( 𝑉 ∩ 𝑈 ) = ∅ )
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	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝐽 ∃ 𝑤 ∈ 𝐽 ( 𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ ( 𝑧 ∩ 𝑤 ) = ∅ ) )