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 46612

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 1914	. . . . . . . 8 ⊢ Ⅎ𝑖𝜑
2		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑖𝑓
3		nfixp1 8937	. . . . . . . . 9 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
4	2, 3	nfel 2914	. . . . . . . 8 ⊢ Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
5	1, 4	nfan 1899	. . . . . . 7 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
6		ixpfn 8922	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 Fn 𝑋)
7	6	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
8		fveq2 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
9	8	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = (-∞(,)(𝐵‘𝑖)))
10		iftrue 4511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = (-∞(,)(𝐵‘𝑖)))
11	9, 10	eqtr4d 2774	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
12		eqimss 4022	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
13	11, 12	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
14		ioossre 13429	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ ℝ
15		iffalse 4514	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = ℝ)
16	14, 15	sseqtrrid 4007	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
17	13, 16	pm2.61i 182	. . . . . . . . . . . . . . 15 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)
18		mnfxr 11297	. . . . . . . . . . . . . . . . 17 ⊢ -∞ ∈ ℝ^*
19	18	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ ∈ ℝ^*)
20		hspdifhsp.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
21	20	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
22	21	rexrd 11290	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
23	22	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
24		hspdifhsp.a	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
25	24	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
26		icossre 13450	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ^*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
27	25, 22, 26	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
28	27	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
29		simpl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
30		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
31		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐴‘𝑖) = (𝐴‘𝑘))
32		fveq2 6881	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐵‘𝑖) = (𝐵‘𝑘))
33	31, 32	oveq12d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑘 → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
34	33	fvixp 8921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
35	29, 30, 34	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
36	35	adantll 714	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
37	28, 36	sseldd 3964	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
38	37	mnfltd 13145	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ < (𝑓‘𝑘))
39	25	rexrd 11290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
40	39	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
41		icoltub 45504	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ^* ∧ (𝐵‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (𝑓‘𝑘) < (𝐵‘𝑘))
42	40, 23, 36, 41	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (𝐵‘𝑘))
43	19, 23, 37, 38, 42	eliood 45494	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (-∞(,)(𝐵‘𝑘)))
44	17, 43	sselid 3961	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
45	44	adantlr 715	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
46	45	ralrimiva 3133	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
47	7, 46	jca 511	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
48		vex 3468	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
49	48	elixp 8923	. . . . . . . . . . 11 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
50	47, 49	sylibr 234	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
51		hspdifhsp.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52		equequ1 2025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → (𝑖 = 𝑙 ↔ 𝑘 = 𝑙))
53	52	ifbid 4529	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
54	53	cbvixpv 8934	. . . . . . . . . . . . . . . 16 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
56	55	mpoeq3ia 7490	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
57	56	mpteq2i 5222	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
58	51, 57	eqtri 2759	. . . . . . . . . . . 12 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
59		hspdifhsp.x	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ Fin)
60	59	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑋 ∈ Fin)
61		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	20	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐵:𝑋⟶ℝ)
63	62, 61	ffvelcdmd 7080	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ)
64	58, 60, 61, 63	hspval 46605	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
65	64	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
66	50, 65	eleqtrrd 2838	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
67	18	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → -∞ ∈ ℝ^*)
68	24	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐴:𝑋⟶ℝ)
69	68, 61	ffvelcdmd 7080	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
70	69	rexrd 11290	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
71	70	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝐴‘𝑖) ∈ ℝ^*)
72		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
73	58, 60, 61, 69	hspval 46605	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
74	73	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
75	72, 74	eleqtrd 2837	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
76	61	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑖 ∈ 𝑋)
77		iftrue 4511	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (-∞(,)(𝐴‘𝑖)))
78	77	fvixp 8921	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
79	75, 76, 78	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
80		iooltub 45506	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐴‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
81	67, 71, 79, 80	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
82	81	adantllr 719	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
83	70	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
84	63	rexrd 11290	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
85	84	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
86	48	elixp 8923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
87	86	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
88	87	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
89		rspa 3235	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
90	88, 89	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
91	90	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
92		icogelb 13418	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑖) ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
93	83, 85, 91, 92	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
94	69	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
95		icossre 13450	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑖) ∈ ℝ ∧ (𝐵‘𝑖) ∈ ℝ^*) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
96	69, 84, 95	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
97	96	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
98	97, 91	sseldd 3964	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
99	94, 98	lenltd 11386	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
100	93, 99	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
101	100	adantr 480	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
102	82, 101	pm2.65da 816	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
103	66, 102	eldifd 3942	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
104	103	ex 412	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝑖 ∈ 𝑋 → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
105	5, 104	ralrimi 3244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
106		eliin 4977	. . . . . . 7 ⊢ (𝑓 ∈ V → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
107	48, 106	ax-mp 5	. . . . . 6 ⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
108	105, 107	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
109	108	ex 412	. . . 4 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
110		hspdifhsp.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ ∅)
111		n0 4333	. . . . . . . . . . 11 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑘 𝑘 ∈ 𝑋)
112	111	biimpi 216	. . . . . . . . . 10 ⊢ (𝑋 ≠ ∅ → ∃𝑘 𝑘 ∈ 𝑋)
113	110, 112	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑘 𝑘 ∈ 𝑋)
114	113	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∃𝑘 𝑘 ∈ 𝑋)
115		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
116		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
117		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
118	117, 32	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
119	117, 31	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))
120	118, 119	difeq12d 4107	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) = ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
121	120	eleq2d 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))))
122	115, 116, 121	eliind 45062	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
123	122	eldifad 3943	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
124	123	adantll 714	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
125		equequ1 2025	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = ℎ → (𝑖 = 𝑙 ↔ ℎ = 𝑙))
126	125	ifbid 4529	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = ℎ → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
127	126	cbvixpv 8934	. . . . . . . . . . . . . . . . 17 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)
128	127	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
129	128	mpoeq3ia 7490	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
130	129	mpteq2i 5222	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
131	51, 130	eqtri 2759	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
132	59	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin)
133		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
134	21	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
135	131, 132, 133, 134	hspval 46605	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝑘(𝐻‘𝑋)(𝐵‘𝑘)) = Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
136	124, 135	eleqtrd 2837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
137		ixpfn 8922	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ) → 𝑓 Fn 𝑋)
138	136, 137	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 Fn 𝑋)
139	138	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
140	139	exlimdv 1933	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (∃𝑘 𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
141	114, 140	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 Fn 𝑋)
142		nfii1 5010	. . . . . . . . . 10 ⊢ Ⅎ𝑖∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
143	2, 142	nfel 2914	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
144	1, 143	nfan 1899	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
145		simpll 766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
146	107	biimpi 216	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
147	146	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
148		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
149		rspa 3235	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
150	147, 148, 149	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
151	150	adantll 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
152		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
153	70	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
154	84	adantlr 715	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
155		simpll 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
156		eldifi 4111	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
157	156	ad2antlr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
158		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
159		ioossre 13429	. . . . . . . . . . . . . 14 ⊢ (-∞(,)(𝐵‘𝑖)) ⊆ ℝ
160		simplr 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
161	64	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
162	160, 161	eleqtrd 2837	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
163		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
164	10	fvixp 8921	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
165	162, 163, 164	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
166	159, 165	sselid 3961	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
167	155, 157, 158, 166	syl21anc 837	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
168	167	rexrd 11290	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ^*)
169		simpl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝜑)
170	156	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
171	169, 170	jca 511	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
172	171	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
173		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑖 ∈ 𝑋)
174		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
175		ixpfn 8922	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → 𝑓 Fn 𝑋)
176	162, 175	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
177	176	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 Fn 𝑋)
178		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝑓‘𝑘) = (𝑓‘𝑖))
179	178	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) = (𝑓‘𝑖))
180	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ ∈ ℝ^*)
181	70	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝐴‘𝑖) ∈ ℝ^*)
182	166	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ ℝ)
183	182	mnfltd 13145	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ < (𝑓‘𝑖))
184		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
185	180, 181, 182, 183, 184	eliood 45494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
186	185	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
187	179, 186	eqeltrd 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
188	187	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
189	77	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
190	189	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
191	188, 190	eleqtrd 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
192	10, 159	eqsstrdi 4008	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
193		ssid 3986	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
194	15, 193	eqsstrdi 4008	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
195	192, 194	pm2.61i 182	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ
196	162	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
197		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
198		fvixp2 45190	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
199	196, 197, 198	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
200	195, 199	sselid 3961	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
201	200	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ ℝ)
202		iffalse 4514	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = ℝ)
203	202	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑘 = 𝑖 → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
204	203	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
205	201, 204	eleqtrd 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
206	205	adantllr 719	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
207	191, 206	pm2.61dan 812	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
208	207	ralrimiva 3133	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
209	177, 208	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
210	48	elixp 8923	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
211	209, 210	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
212	73	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
213	212	ad4ant13 751	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
214	211, 213	eleqtrd 2837	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
215	172, 173, 174, 214	syl21anc 837	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
216		eldifn 4112	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
217	216	ad3antlr 731	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
218	215, 217	pm2.65da 816	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
219	155, 158, 69	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
220	219, 167	lenltd 11386	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
221	218, 220	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
222	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → -∞ ∈ ℝ^*)
223	84	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
224		iooltub 45506	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖))) → (𝑓‘𝑖) < (𝐵‘𝑖))
225	222, 223, 165, 224	syl3anc 1373	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
226	155, 157, 158, 225	syl21anc 837	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
227	153, 154, 168, 221, 226	elicod 13417	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
228	145, 151, 152, 227	syl21anc 837	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
229	228	ex 412	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑖 ∈ 𝑋 → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
230	144, 229	ralrimi 3244	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
231	141, 230	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
232	231, 86	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
233	232	ex 412	. . . 4 ⊢ (𝜑 → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
234	109, 233	impbid 212	. . 3 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
235	234	alrimiv 1927	. 2 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
236		dfcleq 2729	. 2 ⊢ (X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
237	235, 236	sylibr 234	1 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1538 = wceq 1540 ∃wex 1779 ∈ wcel 2109 ≠ wne 2933 ∀wral 3052 Vcvv 3464 ∖ cdif 3928 ⊆ wss 3931 ∅c0 4313 ifcif 4505 ∩ ciin 4973 class class class wbr 5124 ↦ cmpt 5206 Fn wfn 6531 ⟶wf 6532 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 Xcixp 8916 Fincfn 8964 ℝcr 11133 -∞cmnf 11272 ℝ^*cxr 11273 < clt 11274 ≤ cle 11275 (,)cioo 13367 [,)cico 13369

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-pre-lttri 11208 ax-pre-lttrn 11209

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-iin 4975 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-po 5566 df-so 5567 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 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 7993 df-2nd 7994 df-er 8724 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-ioo 13371 df-ico 13373

This theorem is referenced by: hoimbllem 46626

W3C validator