hspdifhsp - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hspdifhsp		Structured version Visualization version GIF version

Theorem hspdifhsp 47300

Description: A n-dimensional half-open interval is the intersection of the difference of half spaces. This is a substep of Proposition 115G (a) of [Fremlin1] p. 32. (Contributed by Glauco Siliprandi, 24-Dec-2020.)

**Hypotheses**
Ref	Expression
hspdifhsp.x	⊢ (𝜑 → 𝑋 ∈ Fin)
hspdifhsp.n	⊢ (𝜑 → 𝑋 ≠ ∅)
hspdifhsp.a	⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
hspdifhsp.b	⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
hspdifhsp.h	⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))

**Assertion**
Ref	Expression
hspdifhsp	⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))

Distinct variable groups: 𝐴,𝑖,𝑙,𝑥,𝑦 𝐵,𝑖,𝑙,𝑥,𝑦 𝑖,𝐻,𝑙,𝑥,𝑦 𝑖,𝑋,𝑙,𝑥,𝑦 𝜑,𝑖,𝑙,𝑥,𝑦

Proof of Theorem hspdifhsp Dummy variables 𝑓 ℎ 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1942	. . . . . . . 8 ⊢ Ⅎ𝑖𝜑
2		nfcv 2923	. . . . . . . . 9 ⊢ Ⅎ𝑖𝑓
3		nfixp1 8915	. . . . . . . . 9 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
4	2, 3	nfel 2937	. . . . . . . 8 ⊢ Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
5	1, 4	nfan 1927	. . . . . . 7 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
6		ixpfn 8900	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 Fn 𝑋)
7	6	ad2antlr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
8		fveq2 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
9	8	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = (-∞(,)(𝐵‘𝑖)))
10		iftrue 4492	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = (-∞(,)(𝐵‘𝑖)))
11	9, 10	eqtr4d 2799	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
12		eqimss 3994	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
13	11, 12	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
14		ioossre 13433	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ ℝ
15		iffalse 4495	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = ℝ)
16	14, 15	sseqtrrid 3979	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
17	13, 16	pm2.61i 184	. . . . . . . . . . . . . . 15 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)
18		mnfxr 11265	. . . . . . . . . . . . . . . . 17 ⊢ -∞ ∈ ℝ^*
19	18	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ ∈ ℝ^*)
20		hspdifhsp.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
21	20	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
22	21	rexrd 11258	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
23	22	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
24		hspdifhsp.a	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
25	24	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
26		icossre 13454	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ^*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
27	25, 22, 26	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
28	27	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
29		simpl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
30		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
31		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐴‘𝑖) = (𝐴‘𝑘))
32		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐵‘𝑖) = (𝐵‘𝑘))
33	31, 32	oveq12d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑘 → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
34	33	fvixp 8899	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
35	29, 30, 34	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
36	35	adantll 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
37	28, 36	sseldd 3937	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
38	37	mnfltd 13148	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ < (𝑓‘𝑘))
39	25	rexrd 11258	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
40	39	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
41		icoltub 46194	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ^* ∧ (𝐵‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (𝑓‘𝑘) < (𝐵‘𝑘))
42	40, 23, 36, 41	syl3anc 1396	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (𝐵‘𝑘))
43	19, 23, 37, 38, 42	eliood 46184	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (-∞(,)(𝐵‘𝑘)))
44	17, 43	sselid 3934	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
45	44	adantlr 727	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
46	45	ralrimiva 3155	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
47	7, 46	jca 520	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
48		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
49	48	elixp 8901	. . . . . . . . . . 11 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
50	47, 49	sylibr 237	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
51		hspdifhsp.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52		equequ1 2053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → (𝑖 = 𝑙 ↔ 𝑘 = 𝑙))
53	52	ifbid 4510	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
54	53	cbvixpv 8912	. . . . . . . . . . . . . . . 16 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
56	55	mpoeq3ia 7488	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
57	56	mpteq2i 5206	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
58	51, 57	eqtri 2784	. . . . . . . . . . . 12 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
59		hspdifhsp.x	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ Fin)
60	59	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑋 ∈ Fin)
61		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	20	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐵:𝑋⟶ℝ)
63	62, 61	ffvelcdmd 7080	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ)
64	58, 60, 61, 63	hspval 47293	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
65	64	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
66	50, 65	eleqtrrd 2864	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
67	18	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → -∞ ∈ ℝ^*)
68	24	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐴:𝑋⟶ℝ)
69	68, 61	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
70	69	rexrd 11258	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
71	70	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝐴‘𝑖) ∈ ℝ^*)
72		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
73	58, 60, 61, 69	hspval 47293	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
74	73	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
75	72, 74	eleqtrd 2863	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
76	61	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑖 ∈ 𝑋)
77		iftrue 4492	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (-∞(,)(𝐴‘𝑖)))
78	77	fvixp 8899	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
79	75, 76, 78	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
80		iooltub 46196	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐴‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
81	67, 71, 79, 80	syl3anc 1396	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
82	81	adantllr 731	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
83	70	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
84	63	rexrd 11258	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
85	84	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
86	48	elixp 8901	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
87	86	biimpi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
88	87	simprd 500	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
89		rspa 3252	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
90	88, 89	sylan 591	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
91	90	adantll 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
92		icogelb 13422	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑖) ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
93	83, 85, 91, 92	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
94	69	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
95		icossre 13454	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑖) ∈ ℝ ∧ (𝐵‘𝑖) ∈ ℝ^*) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
96	69, 84, 95	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
97	96	adantlr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
98	97, 91	sseldd 3937	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
99	94, 98	lenltd 11355	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
100	93, 99	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
101	100	adantr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
102	82, 101	pm2.65da 828	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
103	66, 102	eldifd 3915	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
104	103	ex 417	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝑖 ∈ 𝑋 → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
105	5, 104	ralrimi 3261	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
106		eliin 4960	. . . . . . 7 ⊢ (𝑓 ∈ V → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
107	48, 106	ax-mp 5	. . . . . 6 ⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
108	105, 107	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
109	108	ex 417	. . . 4 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
110		hspdifhsp.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ ∅)
111		n0 4306	. . . . . . . . . . 11 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑘 𝑘 ∈ 𝑋)
112	111	biimpi 219	. . . . . . . . . 10 ⊢ (𝑋 ≠ ∅ → ∃𝑘 𝑘 ∈ 𝑋)
113	110, 112	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑘 𝑘 ∈ 𝑋)
114	113	adantr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∃𝑘 𝑘 ∈ 𝑋)
115		simpl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
116		simpr 489	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
117		id 23	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
118	117, 32	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
119	117, 31	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))
120	118, 119	difeq12d 4081	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) = ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
121	120	eleq2d 2847	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))))
122	115, 116, 121	eliind 45761	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
123	122	eldifad 3916	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
124	123	adantll 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
125		equequ1 2053	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = ℎ → (𝑖 = 𝑙 ↔ ℎ = 𝑙))
126	125	ifbid 4510	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = ℎ → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
127	126	cbvixpv 8912	. . . . . . . . . . . . . . . . 17 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)
128	127	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
129	128	mpoeq3ia 7488	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
130	129	mpteq2i 5206	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
131	51, 130	eqtri 2784	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
132	59	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin)
133		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
134	21	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
135	131, 132, 133, 134	hspval 47293	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝑘(𝐻‘𝑋)(𝐵‘𝑘)) = Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
136	124, 135	eleqtrd 2863	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
137		ixpfn 8900	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ) → 𝑓 Fn 𝑋)
138	136, 137	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 Fn 𝑋)
139	138	ex 417	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
140	139	exlimdv 1961	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (∃𝑘 𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
141	114, 140	mpd 16	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 Fn 𝑋)
142		nfii1 4992	. . . . . . . . . 10 ⊢ Ⅎ𝑖∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
143	2, 142	nfel 2937	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
144	1, 143	nfan 1927	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
145		simpll 778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
146	107	birani 508	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
147		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
148		rspa 3252	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
149	146, 147, 148	syl2anc 595	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
150	149	adantll 726	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
151		simpr 489	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
152	70	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
153	84	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
154		simpll 778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
155		eldifi 4084	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
156	155	ad2antlr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
157		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
158		ioossre 13433	. . . . . . . . . . . . . 14 ⊢ (-∞(,)(𝐵‘𝑖)) ⊆ ℝ
159		simplr 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
160	64	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
161	159, 160	eleqtrd 2863	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
162		simpr 489	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
163	10	fvixp 8899	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
164	161, 162, 163	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
165	158, 164	sselid 3934	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
166	154, 156, 157, 165	syl21anc 850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
167	166	rexrd 11258	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ^*)
168		simpl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝜑)
169	155	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
170	168, 169	jca 520	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
171	170	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
172		simplr 780	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑖 ∈ 𝑋)
173		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
174		ixpfn 8900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → 𝑓 Fn 𝑋)
175	161, 174	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
176	175	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 Fn 𝑋)
177		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝑓‘𝑘) = (𝑓‘𝑖))
178	177	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) = (𝑓‘𝑖))
179	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ ∈ ℝ^*)
180	70	ad4ant13 763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝐴‘𝑖) ∈ ℝ^*)
181	165	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ ℝ)
182	181	mnfltd 13148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ < (𝑓‘𝑖))
183		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
184	179, 180, 181, 182, 183	eliood 46184	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
185	184	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
186	178, 185	eqeltrd 2861	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
187	186	adantlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
188	77	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
189	188	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
190	187, 189	eleqtrd 2863	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
191	10, 158	eqsstrdi 3980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
192		ssid 3958	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
193	15, 192	eqsstrdi 3980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
194	191, 193	pm2.61i 184	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ
195	161	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
196		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
197		fvixp2 45886	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
198	195, 196, 197	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
199	194, 198	sselid 3934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
200	199	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ ℝ)
201		iffalse 4495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = ℝ)
202	201	eqcomd 2767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑘 = 𝑖 → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
203	202	adantl 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
204	200, 203	eleqtrd 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
205	204	adantllr 731	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
206	190, 205	pm2.61dan 824	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
207	206	ralrimiva 3155	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
208	176, 207	jca 520	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
209	48	elixp 8901	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
210	208, 209	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
211	73	eqcomd 2767	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
212	211	ad4ant13 763	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
213	210, 212	eleqtrd 2863	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
214	171, 172, 173, 213	syl21anc 850	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
215		eldifn 4085	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
216	215	ad3antlr 743	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
217	214, 216	pm2.65da 828	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
218	154, 157, 69	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
219	218, 166	lenltd 11355	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
220	217, 219	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
221	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → -∞ ∈ ℝ^*)
222	84	adantlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
223		iooltub 46196	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖))) → (𝑓‘𝑖) < (𝐵‘𝑖))
224	221, 222, 164, 223	syl3anc 1396	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
225	154, 156, 157, 224	syl21anc 850	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
226	152, 153, 167, 220, 225	elicod 13421	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
227	145, 150, 151, 226	syl21anc 850	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
228	227	ex 417	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑖 ∈ 𝑋 → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
229	144, 228	ralrimi 3261	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
230	141, 229	jca 520	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
231	230, 86	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
232	231	ex 417	. . . 4 ⊢ (𝜑 → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
233	109, 232	impbid 215	. . 3 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
234	233	alrimiv 1955	. 2 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
235		dfcleq 2754	. 2 ⊢ (X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
236	234, 235	sylibr 237	1 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∀wal 1566 = wceq 1568 ∃wex 1807 ∈ wcel 2141 ≠ wne 2956 ∀wral 3077 Vcvv 3453 ∖ cdif 3901 ⊆ wss 3904 ∅c0 4285 ifcif 4486 ∩ ciin 4956 class class class wbr 5108 ↦ cmpt 5191 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 Xcixp 8894 Fincfn 8942 ℝcr 11098 -∞cmnf 11240 ℝ^*cxr 11241 < clt 11242 ≤ cle 11243 (,)cioo 13371 [,)cico 13373

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-pre-lttri 11173 ax-pre-lttrn 11174

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-iun 4957 df-iin 4958 df-br 5109 df-opab 5173 df-mpt 5192 df-id 5556 df-po 5569 df-so 5570 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7985 df-2nd 7986 df-er 8693 df-ixp 8895 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-ioo 13375 df-ico 13377

This theorem is referenced by: hoimbllem 47314

W3C validator