ovolicc2lem5

	Ref	Expression
Hypotheses	ovolicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ovolicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ovolicc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	ovolicc2.4	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
	ovolicc2.5	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
	ovolicc2.6	⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
	ovolicc2.7	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
	ovolicc2.8	⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
	ovolicc2.9	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
	ovolicc2.10	⊢ 𝑇 = { 𝑢 ∈ 𝑈 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
Assertion	ovolicc2lem5	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		ovolicc.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ovolicc.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ovolicc.3	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4		ovolicc2.4	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
5		ovolicc2.5	⊢ ( 𝜑 → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
6		ovolicc2.6	⊢ ( 𝜑 → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
7		ovolicc2.7	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
8		ovolicc2.8	⊢ ( 𝜑 → 𝐺 : 𝑈 ⟶ ℕ )
9		ovolicc2.9	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
10		ovolicc2.10	⊢ 𝑇 = { 𝑢 ∈ 𝑈 ∣ ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ }
11	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ^* )
12	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ^* )
13		lbicc2	⊢ ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
14	11 12 3 13	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
15	7 14	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ∪ 𝑈 )
16		eluni2	⊢ ( 𝐴 ∈ ∪ 𝑈 ↔ ∃ 𝑧 ∈ 𝑈 𝐴 ∈ 𝑧 )
17	15 16	sylib	⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑈 𝐴 ∈ 𝑧 )
18	6	elin2d	⊢ ( 𝜑 → 𝑈 ∈ Fin )
19	10	ssrab3	⊢ 𝑇 ⊆ 𝑈
20		ssfi	⊢ ( ( 𝑈 ∈ Fin ∧ 𝑇 ⊆ 𝑈 ) → 𝑇 ∈ Fin )
21	18 19 20	sylancl	⊢ ( 𝜑 → 𝑇 ∈ Fin )
22	7	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
23		ineq1	⊢ ( 𝑢 = 𝑡 → ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) = ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) )
24	23	neeq1d	⊢ ( 𝑢 = 𝑡 → ( ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ↔ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
25	24 10	elrab2	⊢ ( 𝑡 ∈ 𝑇 ↔ ( 𝑡 ∈ 𝑈 ∧ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
26	25	simplbi	⊢ ( 𝑡 ∈ 𝑇 → 𝑡 ∈ 𝑈 )
27		ffvelcdm	⊢ ( ( 𝐺 : 𝑈 ⟶ ℕ ∧ 𝑡 ∈ 𝑈 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℕ )
28	8 26 27	syl2an	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑡 ) ∈ ℕ )
29	5	ffvelcdmda	⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑡 ) ∈ ℕ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
30	28 29	syldan	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( ≤ ∩ ( ℝ × ℝ ) ) )
31	30	elin2d	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( ℝ × ℝ ) )
32		xp2nd	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( ℝ × ℝ ) → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ )
33	31 32	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ )
34	2	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐵 ∈ ℝ )
35	33 34	ifcld	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ℝ )
36	25	simprbi	⊢ ( 𝑡 ∈ 𝑇 → ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
37	36	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
38		n0	⊢ ( ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) )
39	37 38	sylib	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑦 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) )
40	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝐴 ∈ ℝ )
41		simprr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) )
42	41	elin2d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
43	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝐵 ∈ ℝ )
44		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
45	1 43 44	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
46	42 45	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) )
47	46	simp1d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ∈ ℝ )
48	31	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( ℝ × ℝ ) )
49	48 32	syl	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ )
50	46	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝐴 ≤ 𝑦 )
51	41	elin1d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ∈ 𝑡 )
52	28	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝐺 ‘ 𝑡 ) ∈ ℕ )
53		fvco3	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ ( 𝐺 ‘ 𝑡 ) ∈ ℕ ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
54	5 52 53	syl2an2r	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
55	26 9	sylan2	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
56	55	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
57		1st2nd2	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( ℝ × ℝ ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ⟩ )
58	48 57	syl	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) = ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ⟩ )
59	58	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ⟩ ) )
60		df-ov	⊢ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) = ( (,) ‘ ⟨ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ⟩ )
61	59 60	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( (,) ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) = ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) )
62	54 56 61	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑡 = ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) )
63	51 62	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) )
64		xp1st	⊢ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ∈ ( ℝ × ℝ ) → ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ )
65	48 64	syl	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ )
66		rexr	⊢ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ → ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ^* )
67		rexr	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ^* )
68		elioo2	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ^* ∧ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ^* ) → ( 𝑦 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ) )
69	66 67 68	syl2an	⊢ ( ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ ∧ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ ) → ( 𝑦 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ) )
70	65 49 69	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝑦 ∈ ( ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) (,) ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) ) )
71	63 70	mpbid	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → ( 𝑦 ∈ ℝ ∧ ( 1^st ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) < 𝑦 ∧ 𝑦 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) )
72	71	simp3d	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 < ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
73	47 49 72	ltled	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝑦 ≤ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
74	40 47 49 50 73	letrd	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑇 ∧ 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) ) ) → 𝐴 ≤ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
75	74	expr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) )
76	75	exlimdv	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( ∃ 𝑦 𝑦 ∈ ( 𝑡 ∩ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ) )
77	39 76	mpd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐴 ≤ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
78	3	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐴 ≤ 𝐵 )
79		breq2	⊢ ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) = if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) → ( 𝐴 ≤ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ↔ 𝐴 ≤ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ) )
80		breq2	⊢ ( 𝐵 = if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) → ( 𝐴 ≤ 𝐵 ↔ 𝐴 ≤ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ) )
81	79 80	ifboth	⊢ ( ( 𝐴 ≤ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ≤ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) )
82	77 78 81	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → 𝐴 ≤ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) )
83		min2	⊢ ( ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ≤ 𝐵 )
84	33 34 83	syl2anc	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ≤ 𝐵 )
85		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ℝ ∧ 𝐴 ≤ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ≤ 𝐵 ) ) )
86	1 2 85	syl2anc	⊢ ( 𝜑 → ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ℝ ∧ 𝐴 ≤ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ≤ 𝐵 ) ) )
87	86	adantr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ℝ ∧ 𝐴 ≤ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ≤ 𝐵 ) ) )
88	35 82 84 87	mpbir3and	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐴 [,] 𝐵 ) )
89	22 88	sseldd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ∪ 𝑈 )
90		eluni2	⊢ ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ∪ 𝑈 ↔ ∃ 𝑥 ∈ 𝑈 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 )
91	89 90	sylib	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑥 ∈ 𝑈 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 )
92		simprl	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑥 ∈ 𝑈 ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ) ) → 𝑥 ∈ 𝑈 )
93		simprr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑥 ∈ 𝑈 ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ) ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 )
94	88	adantr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑥 ∈ 𝑈 ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ) ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐴 [,] 𝐵 ) )
95		inelcm	⊢ ( ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
96	93 94 95	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑥 ∈ 𝑈 ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ) ) → ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
97		ineq1	⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) = ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) )
98	97	neeq1d	⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ↔ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
99	98 10	elrab2	⊢ ( 𝑥 ∈ 𝑇 ↔ ( 𝑥 ∈ 𝑈 ∧ ( 𝑥 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
100	92 96 99	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) ∧ ( 𝑥 ∈ 𝑈 ∧ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ) ) → 𝑥 ∈ 𝑇 )
101	91 100 93	reximssdv	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝑇 ) → ∃ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 )
102	101	ralrimiva	⊢ ( 𝜑 → ∀ 𝑡 ∈ 𝑇 ∃ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 )
103		eleq2	⊢ ( 𝑥 = ( ℎ ‘ 𝑡 ) → ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ↔ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) ) )
104	103	ac6sfi	⊢ ( ( 𝑇 ∈ Fin ∧ ∀ 𝑡 ∈ 𝑇 ∃ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ 𝑥 ) → ∃ ℎ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) ) )
105	21 102 104	syl2anc	⊢ ( 𝜑 → ∃ ℎ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) ) )
106	105	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ) → ∃ ℎ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) ) )
107		2fveq3	⊢ ( 𝑥 = 𝑡 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) )
108	107	fveq2d	⊢ ( 𝑥 = 𝑡 → ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) = ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) )
109	108	breq1d	⊢ ( 𝑥 = 𝑡 → ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 ↔ ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 ) )
110	109 108	ifbieq1d	⊢ ( 𝑥 = 𝑡 → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) = if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) )
111		fveq2	⊢ ( 𝑥 = 𝑡 → ( ℎ ‘ 𝑥 ) = ( ℎ ‘ 𝑡 ) )
112	110 111	eleq12d	⊢ ( 𝑥 = 𝑡 → ( if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ↔ if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) ) )
113	112	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ↔ ∀ 𝑡 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) )
114	1	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝐴 ∈ ℝ )
115	2	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝐵 ∈ ℝ )
116	3	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝐴 ≤ 𝐵 )
117	5	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
118	6	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝑈 ∈ ( 𝒫 ran ( (,) ∘ 𝐹 ) ∩ Fin ) )
119	7	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
120	8	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝐺 : 𝑈 ⟶ ℕ )
121	9	adantlr	⊢ ( ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) ∧ 𝑡 ∈ 𝑈 ) → ( ( (,) ∘ 𝐹 ) ‘ ( 𝐺 ‘ 𝑡 ) ) = 𝑡 )
122		simprrl	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → ℎ : 𝑇 ⟶ 𝑇 )
123		simprrr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) )
124	112	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) )
125	123 124	sylan	⊢ ( ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) ∧ 𝑡 ∈ 𝑇 ) → if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) )
126		simprlr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝐴 ∈ 𝑧 )
127		simprll	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝑧 ∈ 𝑈 )
128	14	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
129		inelcm	⊢ ( ( 𝐴 ∈ 𝑧 ∧ 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
130	126 128 129	syl2anc	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ )
131		ineq1	⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) = ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) )
132	131	neeq1d	⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ↔ ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
133	132 10	elrab2	⊢ ( 𝑧 ∈ 𝑇 ↔ ( 𝑧 ∈ 𝑈 ∧ ( 𝑧 ∩ ( 𝐴 [,] 𝐵 ) ) ≠ ∅ ) )
134	127 130 133	sylanbrc	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → 𝑧 ∈ 𝑇 )
135		eqid	⊢ seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) = seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) )
136		fveq2	⊢ ( 𝑚 = 𝑛 → ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑚 ) = ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑛 ) )
137	136	eleq2d	⊢ ( 𝑚 = 𝑛 → ( 𝐵 ∈ ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑚 ) ↔ 𝐵 ∈ ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑛 ) ) )
138	137	cbvrabv	⊢ { 𝑚 ∈ ℕ ∣ 𝐵 ∈ ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑚 ) } = { 𝑛 ∈ ℕ ∣ 𝐵 ∈ ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑛 ) }
139		eqid	⊢ inf ( { 𝑚 ∈ ℕ ∣ 𝐵 ∈ ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑚 ) } , ℝ , < ) = inf ( { 𝑚 ∈ ℕ ∣ 𝐵 ∈ ( seq 1 ( ( ℎ ∘ 1^st ) , ( ℕ × { 𝑧 } ) ) ‘ 𝑚 ) } , ℝ , < )
140	114 115 116 4 117 118 119 120 121 10 122 125 126 134 135 138 139	ovolicc2lem4	⊢ ( ( 𝜑 ∧ ( ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
141	140	anassrs	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
142	141	expr	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ℎ : 𝑇 ⟶ 𝑇 ) → ( ∀ 𝑥 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑥 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑥 ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) ) )
143	113 142	biimtrrid	⊢ ( ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ℎ : 𝑇 ⟶ 𝑇 ) → ( ∀ 𝑡 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) ) )
144	143	expimpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ) → ( ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) ) )
145	144	exlimdv	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ) → ( ∃ ℎ ( ℎ : 𝑇 ⟶ 𝑇 ∧ ∀ 𝑡 ∈ 𝑇 if ( ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) ≤ 𝐵 , ( 2^nd ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑡 ) ) ) , 𝐵 ) ∈ ( ℎ ‘ 𝑡 ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) ) )
146	106 145	mpd	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝑈 ∧ 𝐴 ∈ 𝑧 ) ) → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )
147	17 146	rexlimddv	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ≤ sup ( ran 𝑆 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem ovolicc2lem5

Proof