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 46144

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 1909	. . . . . . . 8 ⊢ Ⅎ𝑖𝜑
2		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑖𝑓
3		nfixp1 8937	. . . . . . . . 9 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
4	2, 3	nfel 2906	. . . . . . . 8 ⊢ Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
5	1, 4	nfan 1894	. . . . . . 7 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
6		ixpfn 8922	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 Fn 𝑋)
7	6	ad2antlr 725	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
8		fveq2 6896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
9	8	oveq2d 7435	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = (-∞(,)(𝐵‘𝑖)))
10		iftrue 4536	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = (-∞(,)(𝐵‘𝑖)))
11	9, 10	eqtr4d 2768	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
12		eqimss 4035	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
13	11, 12	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
14		ioossre 13425	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ ℝ
15		iffalse 4539	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = ℝ)
16	14, 15	sseqtrrid 4030	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
17	13, 16	pm2.61i 182	. . . . . . . . . . . . . . 15 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)
18		mnfxr 11308	. . . . . . . . . . . . . . . . 17 ⊢ -∞ ∈ ℝ^*
19	18	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ ∈ ℝ^*)
20		hspdifhsp.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
21	20	ffvelcdmda 7093	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
22	21	rexrd 11301	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
23	22	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
24		hspdifhsp.a	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
25	24	ffvelcdmda 7093	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
26		icossre 13445	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ^*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
27	25, 22, 26	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
28	27	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
29		simpl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
30		simpr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
31		fveq2 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐴‘𝑖) = (𝐴‘𝑘))
32		fveq2 6896	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐵‘𝑖) = (𝐵‘𝑘))
33	31, 32	oveq12d 7437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑘 → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
34	33	fvixp 8921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
35	29, 30, 34	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
36	35	adantll 712	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
37	28, 36	sseldd 3977	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
38	37	mnfltd 13144	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ < (𝑓‘𝑘))
39	25	rexrd 11301	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
40	39	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
41		icoltub 45033	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ^* ∧ (𝐵‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (𝑓‘𝑘) < (𝐵‘𝑘))
42	40, 23, 36, 41	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (𝐵‘𝑘))
43	19, 23, 37, 38, 42	eliood 45023	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (-∞(,)(𝐵‘𝑘)))
44	17, 43	sselid 3974	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
45	44	adantlr 713	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
46	45	ralrimiva 3135	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
47	7, 46	jca 510	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
48		vex 3465	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
49	48	elixp 8923	. . . . . . . . . . 11 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
50	47, 49	sylibr 233	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
51		hspdifhsp.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52		equequ1 2020	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → (𝑖 = 𝑙 ↔ 𝑘 = 𝑙))
53	52	ifbid 4553	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
54	53	cbvixpv 8934	. . . . . . . . . . . . . . . 16 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
56	55	mpoeq3ia 7498	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
57	56	mpteq2i 5254	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
58	51, 57	eqtri 2753	. . . . . . . . . . . 12 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
59		hspdifhsp.x	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ Fin)
60	59	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑋 ∈ Fin)
61		simpr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	20	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐵:𝑋⟶ℝ)
63	62, 61	ffvelcdmd 7094	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ)
64	58, 60, 61, 63	hspval 46137	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
65	64	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
66	50, 65	eleqtrrd 2828	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
67	18	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → -∞ ∈ ℝ^*)
68	24	adantr 479	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐴:𝑋⟶ℝ)
69	68, 61	ffvelcdmd 7094	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
70	69	rexrd 11301	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
71	70	adantr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝐴‘𝑖) ∈ ℝ^*)
72		simpr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
73	58, 60, 61, 69	hspval 46137	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
74	73	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
75	72, 74	eleqtrd 2827	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
76	61	adantr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑖 ∈ 𝑋)
77		iftrue 4536	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (-∞(,)(𝐴‘𝑖)))
78	77	fvixp 8921	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
79	75, 76, 78	syl2anc 582	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
80		iooltub 45035	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐴‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
81	67, 71, 79, 80	syl3anc 1368	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
82	81	adantllr 717	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
83	70	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
84	63	rexrd 11301	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
85	84	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
86	48	elixp 8923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
87	86	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
88	87	simprd 494	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
89		rspa 3235	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
90	88, 89	sylan 578	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
91	90	adantll 712	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
92		icogelb 13415	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑖) ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
93	83, 85, 91, 92	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
94	69	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
95		icossre 13445	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑖) ∈ ℝ ∧ (𝐵‘𝑖) ∈ ℝ^*) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
96	69, 84, 95	syl2anc 582	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
97	96	adantlr 713	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
98	97, 91	sseldd 3977	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
99	94, 98	lenltd 11397	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
100	93, 99	mpbid 231	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
101	100	adantr 479	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
102	82, 101	pm2.65da 815	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
103	66, 102	eldifd 3955	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
104	103	ex 411	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝑖 ∈ 𝑋 → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
105	5, 104	ralrimi 3244	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
106		eliin 5002	. . . . . . 7 ⊢ (𝑓 ∈ V → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
107	48, 106	ax-mp 5	. . . . . 6 ⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
108	105, 107	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
109	108	ex 411	. . . 4 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
110		hspdifhsp.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ ∅)
111		n0 4346	. . . . . . . . . . 11 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑘 𝑘 ∈ 𝑋)
112	111	biimpi 215	. . . . . . . . . 10 ⊢ (𝑋 ≠ ∅ → ∃𝑘 𝑘 ∈ 𝑋)
113	110, 112	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑘 𝑘 ∈ 𝑋)
114	113	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∃𝑘 𝑘 ∈ 𝑋)
115		simpl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
116		simpr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
117		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
118	117, 32	oveq12d 7437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
119	117, 31	oveq12d 7437	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))
120	118, 119	difeq12d 4119	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) = ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
121	120	eleq2d 2811	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))))
122	115, 116, 121	eliind 44579	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
123	122	eldifad 3956	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
124	123	adantll 712	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
125		equequ1 2020	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = ℎ → (𝑖 = 𝑙 ↔ ℎ = 𝑙))
126	125	ifbid 4553	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = ℎ → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
127	126	cbvixpv 8934	. . . . . . . . . . . . . . . . 17 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)
128	127	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
129	128	mpoeq3ia 7498	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
130	129	mpteq2i 5254	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
131	51, 130	eqtri 2753	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
132	59	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin)
133		simpr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
134	21	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
135	131, 132, 133, 134	hspval 46137	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝑘(𝐻‘𝑋)(𝐵‘𝑘)) = Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
136	124, 135	eleqtrd 2827	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
137		ixpfn 8922	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ) → 𝑓 Fn 𝑋)
138	136, 137	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 Fn 𝑋)
139	138	ex 411	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
140	139	exlimdv 1928	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (∃𝑘 𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
141	114, 140	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 Fn 𝑋)
142		nfii1 5033	. . . . . . . . . 10 ⊢ Ⅎ𝑖∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
143	2, 142	nfel 2906	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
144	1, 143	nfan 1894	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
145		simpll 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
146	107	biimpi 215	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
147	146	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
148		simpr 483	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
149		rspa 3235	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
150	147, 148, 149	syl2anc 582	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
151	150	adantll 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
152		simpr 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
153	70	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
154	84	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
155		simpll 765	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
156		eldifi 4123	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
157	156	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
158		simpr 483	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
159		ioossre 13425	. . . . . . . . . . . . . 14 ⊢ (-∞(,)(𝐵‘𝑖)) ⊆ ℝ
160		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
161	64	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
162	160, 161	eleqtrd 2827	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
163		simpr 483	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
164	10	fvixp 8921	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
165	162, 163, 164	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
166	159, 165	sselid 3974	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
167	155, 157, 158, 166	syl21anc 836	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
168	167	rexrd 11301	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ^*)
169		simpl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝜑)
170	156	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
171	169, 170	jca 510	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
172	171	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
173		simplr 767	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑖 ∈ 𝑋)
174		simpr 483	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
175		ixpfn 8922	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → 𝑓 Fn 𝑋)
176	162, 175	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
177	176	adantr 479	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 Fn 𝑋)
178		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝑓‘𝑘) = (𝑓‘𝑖))
179	178	adantl 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) = (𝑓‘𝑖))
180	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ ∈ ℝ^*)
181	70	ad4ant13 749	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝐴‘𝑖) ∈ ℝ^*)
182	166	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ ℝ)
183	182	mnfltd 13144	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ < (𝑓‘𝑖))
184		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
185	180, 181, 182, 183, 184	eliood 45023	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
186	185	adantr 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
187	179, 186	eqeltrd 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
188	187	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
189	77	eqcomd 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
190	189	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
191	188, 190	eleqtrd 2827	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
192	10, 159	eqsstrdi 4031	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
193		ssid 3999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
194	15, 193	eqsstrdi 4031	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
195	192, 194	pm2.61i 182	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ
196	162	adantr 479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
197		simpr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
198		fvixp2 44713	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
199	196, 197, 198	syl2anc 582	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
200	195, 199	sselid 3974	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
201	200	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ ℝ)
202		iffalse 4539	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = ℝ)
203	202	eqcomd 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑘 = 𝑖 → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
204	203	adantl 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
205	201, 204	eleqtrd 2827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
206	205	adantllr 717	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
207	191, 206	pm2.61dan 811	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
208	207	ralrimiva 3135	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
209	177, 208	jca 510	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
210	48	elixp 8923	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
211	209, 210	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
212	73	eqcomd 2731	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
213	212	ad4ant13 749	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
214	211, 213	eleqtrd 2827	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
215	172, 173, 174, 214	syl21anc 836	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
216		eldifn 4124	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
217	216	ad3antlr 729	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
218	215, 217	pm2.65da 815	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
219	155, 158, 69	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
220	219, 167	lenltd 11397	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
221	218, 220	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
222	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → -∞ ∈ ℝ^*)
223	84	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
224		iooltub 45035	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖))) → (𝑓‘𝑖) < (𝐵‘𝑖))
225	222, 223, 165, 224	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
226	155, 157, 158, 225	syl21anc 836	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
227	153, 154, 168, 221, 226	elicod 13414	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
228	145, 151, 152, 227	syl21anc 836	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
229	228	ex 411	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑖 ∈ 𝑋 → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
230	144, 229	ralrimi 3244	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
231	141, 230	jca 510	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
232	231, 86	sylibr 233	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
233	232	ex 411	. . . 4 ⊢ (𝜑 → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
234	109, 233	impbid 211	. . 3 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
235	234	alrimiv 1922	. 2 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
236		dfcleq 2718	. 2 ⊢ (X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
237	235, 236	sylibr 233	1 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∀wal 1531 = wceq 1533 ∃wex 1773 ∈ wcel 2098 ≠ wne 2929 ∀wral 3050 Vcvv 3461 ∖ cdif 3941 ⊆ wss 3944 ∅c0 4322 ifcif 4530 ∩ ciin 4998 class class class wbr 5149 ↦ cmpt 5232 Fn wfn 6544 ⟶wf 6545 ‘cfv 6549 (class class class)co 7419 ∈ cmpo 7421 Xcixp 8916 Fincfn 8964 ℝcr 11144 -∞cmnf 11283 ℝ^*cxr 11284 < clt 11285 ≤ cle 11286 (,)cioo 13364 [,)cico 13366

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 ax-cnex 11201 ax-resscn 11202 ax-pre-lttri 11219 ax-pre-lttrn 11220

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-nel 3036 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3419 df-v 3463 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-iun 4999 df-iin 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-po 5590 df-so 5591 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-ima 5691 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 df-fo 6555 df-f1o 6556 df-fv 6557 df-ov 7422 df-oprab 7423 df-mpo 7424 df-1st 7994 df-2nd 7995 df-er 8725 df-ixp 8917 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11287 df-mnf 11288 df-xr 11289 df-ltxr 11290 df-le 11291 df-ioo 13368 df-ico 13370

This theorem is referenced by: hoimbllem 46158

W3C validator