uniioombllem2a

	Ref	Expression
Hypotheses	uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
	uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
	uniioombl.a	⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
	uniioombl.e	⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
	uniioombl.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
	uniioombl.g	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	uniioombl.s	⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
	uniioombl.t	⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
	uniioombl.v	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
Assertion	uniioombllem2a	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ran (,) )

Proof

Step	Hyp	Ref	Expression
1		uniioombl.1	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
2		uniioombl.2	⊢ ( 𝜑 → Disj 𝑥 ∈ ℕ ( (,) ‘ ( 𝐹 ‘ 𝑥 ) ) )
3		uniioombl.3	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
4		uniioombl.a	⊢ 𝐴 = ∪ ran ( (,) ∘ 𝐹 )
5		uniioombl.e	⊢ ( 𝜑 → ( vol* ‘ 𝐸 ) ∈ ℝ )
6		uniioombl.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ⁺ )
7		uniioombl.g	⊢ ( 𝜑 → 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
8		uniioombl.s	⊢ ( 𝜑 → 𝐸 ⊆ ∪ ran ( (,) ∘ 𝐺 ) )
9		uniioombl.t	⊢ 𝑇 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐺 ) )
10		uniioombl.v	⊢ ( 𝜑 → sup ( ran 𝑇 , ℝ^* , < ) ≤ ( ( vol* ‘ 𝐸 ) + 𝐶 ) )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
12	11	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
13	12	elin2d	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ × ℝ ) )
14		1st2nd2	⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ 𝑧 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
15	13 14	syl	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 𝐹 ‘ 𝑧 ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
16	15	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ ) )
17		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ⟩ )
18	16 17	eqtr4di	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) = ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
19	7	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
20	19	elin2d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) ∈ ( ℝ × ℝ ) )
21		1st2nd2	⊢ ( ( 𝐺 ‘ 𝐽 ) ∈ ( ℝ × ℝ ) → ( 𝐺 ‘ 𝐽 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ )
22	20 21	syl	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 𝐺 ‘ 𝐽 ) = ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ )
23	22	fveq2d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ ) )
24		df-ov	⊢ ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ⟩ )
25	23 24	eqtr4di	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) = ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
27	18 26	ineq12d	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) ∩ ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
28		ovolfcl	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝑧 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
29	11 28	sylan	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
30	29	simp1d	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
31	30	rexrd	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ^* )
32	29	simp2d	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
33	32	rexrd	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ^* )
34		ovolfcl	⊢ ( ( 𝐺 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐽 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
35	7 34	sylan	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ ∧ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) )
36	35	simp1d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ )
37	36	rexrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ^* )
38	37	adantr	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ^* )
39	35	simp2d	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ )
40	39	rexrd	⊢ ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ^* )
41	40	adantr	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ^* )
42		iooin	⊢ ( ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ^* ∧ ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ^* ) ∧ ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ^* ∧ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ∈ ℝ^* ) ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) ∩ ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) = ( if ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
43	31 33 38 41 42	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ) ∩ ( ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) (,) ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) = ( if ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
44	27 43	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) = ( if ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) )
45		ioorebas	⊢ ( if ( ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 1^st ‘ ( 𝐹 ‘ 𝑧 ) ) ) (,) if ( ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) , ( 2^nd ‘ ( 𝐹 ‘ 𝑧 ) ) , ( 2^nd ‘ ( 𝐺 ‘ 𝐽 ) ) ) ) ∈ ran (,)
46	44 45	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝐽 ∈ ℕ ) ∧ 𝑧 ∈ ℕ ) → ( ( (,) ‘ ( 𝐹 ‘ 𝑧 ) ) ∩ ( (,) ‘ ( 𝐺 ‘ 𝐽 ) ) ) ∈ ran (,) )

Metamath Proof Explorer

Theorem uniioombllem2a

Proof