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 41402

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 2009	. . . . . . . 8 ⊢ Ⅎ𝑖𝜑
2		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑖𝑓
3		nfixp1 8133	. . . . . . . . 9 ⊢ Ⅎ𝑖X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
4	2, 3	nfel 2920	. . . . . . . 8 ⊢ Ⅎ𝑖 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))
5	1, 4	nfan 1998	. . . . . . 7 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
6		ixpfn 8119	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 Fn 𝑋)
7	6	ad2antlr 718	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
8		fveq2 6375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 = 𝑖 → (𝐵‘𝑘) = (𝐵‘𝑖))
9	8	oveq2d 6858	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = (-∞(,)(𝐵‘𝑖)))
10		iftrue 4249	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = (-∞(,)(𝐵‘𝑖)))
11	9, 10	eqtr4d 2802	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
12		eqimss 3817	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞(,)(𝐵‘𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
13	11, 12	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
14		ioossre 12437	. . . . . . . . . . . . . . . . 17 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ ℝ
15		iffalse 4252	. . . . . . . . . . . . . . . . 17 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) = ℝ)
16	14, 15	syl5sseqr 3814	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑘 = 𝑖 → (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
17	13, 16	pm2.61i 176	. . . . . . . . . . . . . . 15 ⊢ (-∞(,)(𝐵‘𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)
18		mnfxr 10350	. . . . . . . . . . . . . . . . 17 ⊢ -∞ ∈ ℝ^*
19	18	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ ∈ ℝ^*)
20		hspdifhsp.b	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
21	20	ffvelrnda 6549	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
22	21	rexrd 10343	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
23	22	adantlr 706	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ^*)
24		hspdifhsp.a	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
25	24	ffvelrnda 6549	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ)
26		icossre 12456	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ^*) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
27	25, 22, 26	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
28	27	adantlr 706	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) ⊆ ℝ)
29		simpl 474	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
30		simpr 477	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
31		fveq2 6375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐴‘𝑖) = (𝐴‘𝑘))
32		fveq2 6375	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑘 → (𝐵‘𝑖) = (𝐵‘𝑘))
33	31, 32	oveq12d 6860	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑘 → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
34	33	fvixp 8118	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
35	29, 30, 34	syl2anc 579	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
36	35	adantll 705	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
37	28, 36	sseldd 3762	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
38	37	mnfltd 12158	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → -∞ < (𝑓‘𝑘))
39	25	rexrd 10343	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
40	39	adantlr 706	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝐴‘𝑘) ∈ ℝ^*)
41		icoltub 40305	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝑘) ∈ ℝ^* ∧ (𝐵‘𝑘) ∈ ℝ^* ∧ (𝑓‘𝑘) ∈ ((𝐴‘𝑘)[,)(𝐵‘𝑘))) → (𝑓‘𝑘) < (𝐵‘𝑘))
42	40, 23, 36, 41	syl3anc 1490	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) < (𝐵‘𝑘))
43	19, 23, 37, 38, 42	eliood 40294	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ (-∞(,)(𝐵‘𝑘)))
44	17, 43	sseldi 3759	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
45	44	adantlr 706	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
46	45	ralrimiva 3113	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
47	7, 46	jca 507	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
48		vex 3353	. . . . . . . . . . . 12 ⊢ 𝑓 ∈ V
49	48	elixp 8120	. . . . . . . . . . 11 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ)))
50	47, 49	sylibr 225	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
51		hspdifhsp.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52		equequ1 2122	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → (𝑖 = 𝑙 ↔ 𝑘 = 𝑙))
53	52	ifbid 4265	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
54	53	cbvixpv 8131	. . . . . . . . . . . . . . . 16 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)
55	54	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
56	55	mpt2eq3ia 6918	. . . . . . . . . . . . . 14 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
57	56	mpteq2i 4900	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
58	51, 57	eqtri 2787	. . . . . . . . . . . 12 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑘 ∈ 𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
59		hspdifhsp.x	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ Fin)
60	59	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑋 ∈ Fin)
61		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
62	20	adantr 472	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐵:𝑋⟶ℝ)
63	62, 61	ffvelrnd 6550	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ)
64	58, 60, 61, 63	hspval 41395	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
65	64	adantlr 706	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
66	50, 65	eleqtrrd 2847	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
67	18	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → -∞ ∈ ℝ^*)
68	24	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → 𝐴:𝑋⟶ℝ)
69	68, 61	ffvelrnd 6550	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
70	69	rexrd 10343	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
71	70	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝐴‘𝑖) ∈ ℝ^*)
72		simpr 477	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
73	58, 60, 61, 69	hspval 41395	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
74	73	adantr 472	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
75	72, 74	eleqtrd 2846	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
76	61	adantr 472	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑖 ∈ 𝑋)
77		iftrue 4249	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (-∞(,)(𝐴‘𝑖)))
78	77	fvixp 8118	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
79	75, 76, 78	syl2anc 579	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
80		iooltub 40307	. . . . . . . . . . . 12 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐴‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
81	67, 71, 79, 80	syl3anc 1490	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
82	81	adantllr 710	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → (𝑓‘𝑖) < (𝐴‘𝑖))
83	70	adantlr 706	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
84	63	rexrd 10343	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
85	84	adantlr 706	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
86	48	elixp 8120	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
87	86	biimpi 207	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
88	87	simprd 489	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
89		rspa 3077	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
90	88, 89	sylan 575	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
91	90	adantll 705	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
92		icogelb 12427	. . . . . . . . . . . . 13 ⊢ (((𝐴‘𝑖) ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
93	83, 85, 91, 92	syl3anc 1490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
94	69	adantlr 706	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
95		icossre 12456	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝑖) ∈ ℝ ∧ (𝐵‘𝑖) ∈ ℝ^*) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
96	69, 84, 95	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
97	96	adantlr 706	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ⊆ ℝ)
98	97, 91	sseldd 3762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
99	94, 98	lenltd 10437	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
100	93, 99	mpbid 223	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
101	100	adantr 472	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
102	82, 101	pm2.65da 851	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
103	66, 102	eldifd 3743	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
104	103	ex 401	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → (𝑖 ∈ 𝑋 → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
105	5, 104	ralrimi 3104	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
106		eliin 4681	. . . . . . 7 ⊢ (𝑓 ∈ V → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
107	48, 106	ax-mp 5	. . . . . 6 ⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
108	105, 107	sylibr 225	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
109	108	ex 401	. . . 4 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
110		hspdifhsp.n	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ ∅)
111		n0 4095	. . . . . . . . . . 11 ⊢ (𝑋 ≠ ∅ ↔ ∃𝑘 𝑘 ∈ 𝑋)
112	111	biimpi 207	. . . . . . . . . 10 ⊢ (𝑋 ≠ ∅ → ∃𝑘 𝑘 ∈ 𝑋)
113	110, 112	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑘 𝑘 ∈ 𝑋)
114	113	adantr 472	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∃𝑘 𝑘 ∈ 𝑋)
115		simpl 474	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
116		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
117		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑘 → 𝑖 = 𝑘)
118	117, 32	oveq12d 6860	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
119	117, 31	oveq12d 6860	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑘 → (𝑖(𝐻‘𝑋)(𝐴‘𝑖)) = (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))
120	118, 119	difeq12d 3891	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) = ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
121	120	eleq2d 2830	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘)))))
122	115, 116, 121	eliind 39823	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ ((𝑘(𝐻‘𝑋)(𝐵‘𝑘)) ∖ (𝑘(𝐻‘𝑋)(𝐴‘𝑘))))
123	122	eldifad 3744	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
124	123	adantll 705	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ (𝑘(𝐻‘𝑋)(𝐵‘𝑘)))
125		equequ1 2122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = ℎ → (𝑖 = 𝑙 ↔ ℎ = 𝑙))
126	125	ifbid 4265	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = ℎ → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
127	126	cbvixpv 8131	. . . . . . . . . . . . . . . . 17 ⊢ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)
128	127	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝑙 ∈ 𝑥 ∧ 𝑦 ∈ ℝ) → X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
129	128	mpt2eq3ia 6918	. . . . . . . . . . . . . . 15 ⊢ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ))
130	129	mpteq2i 4900	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ X𝑖 ∈ 𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
131	51, 130	eqtri 2787	. . . . . . . . . . . . 13 ⊢ 𝐻 = (𝑥 ∈ Fin ↦ (𝑙 ∈ 𝑥, 𝑦 ∈ ℝ ↦ Xℎ ∈ 𝑥 if(ℎ = 𝑙, (-∞(,)𝑦), ℝ)))
132	59	ad2antrr 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑋 ∈ Fin)
133		simpr 477	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
134	21	adantlr 706	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝐵‘𝑘) ∈ ℝ)
135	131, 132, 133, 134	hspval 41395	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → (𝑘(𝐻‘𝑋)(𝐵‘𝑘)) = Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
136	124, 135	eleqtrd 2846	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ))
137		ixpfn 8119	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Xℎ ∈ 𝑋 if(ℎ = 𝑘, (-∞(,)(𝐵‘𝑘)), ℝ) → 𝑓 Fn 𝑋)
138	136, 137	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑘 ∈ 𝑋) → 𝑓 Fn 𝑋)
139	138	ex 401	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
140	139	exlimdv 2028	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (∃𝑘 𝑘 ∈ 𝑋 → 𝑓 Fn 𝑋))
141	114, 140	mpd 15	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 Fn 𝑋)
142		nfii1 4707	. . . . . . . . . 10 ⊢ Ⅎ𝑖∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
143	2, 142	nfel 2920	. . . . . . . . 9 ⊢ Ⅎ𝑖 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
144	1, 143	nfan 1998	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
145		simpll 783	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
146	107	biimpi 207	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
147	146	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → ∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
148		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
149		rspa 3077	. . . . . . . . . . . 12 ⊢ ((∀𝑖 ∈ 𝑋 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
150	147, 148, 149	syl2anc 579	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
151	150	adantll 705	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))
152		simpr 477	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
153	70	adantlr 706	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ^*)
154	84	adantlr 706	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
155		simpll 783	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝜑)
156		eldifi 3894	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
157	156	ad2antlr 718	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
158		simpr 477	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
159		ioossre 12437	. . . . . . . . . . . . . 14 ⊢ (-∞(,)(𝐵‘𝑖)) ⊆ ℝ
160		simplr 785	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
161	64	adantlr 706	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑖(𝐻‘𝑋)(𝐵‘𝑖)) = X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
162	160, 161	eleqtrd 2846	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
163		simpr 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑖 ∈ 𝑋)
164	10	fvixp 8118	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
165	162, 163, 164	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖)))
166	159, 165	sseldi 3759	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
167	155, 157, 158, 166	syl21anc 866	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ)
168	167	rexrd 10343	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ℝ^*)
169		simpl 474	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝜑)
170	156	adantl 473	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖)))
171	169, 170	jca 507	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
172	171	ad2antrr 717	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))))
173		simplr 785	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑖 ∈ 𝑋)
174		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
175		ixpfn 8119	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) → 𝑓 Fn 𝑋)
176	162, 175	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → 𝑓 Fn 𝑋)
177	176	adantr 472	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 Fn 𝑋)
178		fveq2 6375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑘 = 𝑖 → (𝑓‘𝑘) = (𝑓‘𝑖))
179	178	adantl 473	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) = (𝑓‘𝑖))
180	18	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ ∈ ℝ^*)
181	70	ad4ant13 757	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝐴‘𝑖) ∈ ℝ^*)
182	166	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ ℝ)
183	182	mnfltd 12158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → -∞ < (𝑓‘𝑖))
184		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) < (𝐴‘𝑖))
185	180, 181, 182, 183, 184	eliood 40294	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
186	185	adantr 472	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑖) ∈ (-∞(,)(𝐴‘𝑖)))
187	179, 186	eqeltrd 2844	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
188	187	adantlr 706	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ (-∞(,)(𝐴‘𝑖)))
189	77	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 = 𝑖 → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
190	189	adantl 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (-∞(,)(𝐴‘𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
191	188, 190	eleqtrd 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
192	10, 159	syl6eqss 3815	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
193		ssid 3783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℝ ⊆ ℝ
194	15, 193	syl6eqss 3815	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ)
195	192, 194	pm2.61i 176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ⊆ ℝ
196	162	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
197		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → 𝑘 ∈ 𝑋)
198		fvixp2 39967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
199	196, 197, 198	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵‘𝑖)), ℝ))
200	195, 199	sseldi 3759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ ℝ)
201	200	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ ℝ)
202		iffalse 4252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = ℝ)
203	202	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ 𝑘 = 𝑖 → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
204	203	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
205	201, 204	eleqtrd 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
206	205	adantllr 710	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
207	191, 206	pm2.61dan 847	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) ∧ 𝑘 ∈ 𝑋) → (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
208	207	ralrimiva 3113	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
209	177, 208	jca 507	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
210	48	elixp 8120	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘 ∈ 𝑋 (𝑓‘𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ)))
211	209, 210	sylibr 225	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ))
212	73	eqcomd 2771	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑋) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
213	212	ad4ant13 757	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → X𝑘 ∈ 𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴‘𝑖)), ℝ) = (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
214	211, 213	eleqtrd 2846	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
215	172, 173, 174, 214	syl21anc 866	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
216		eldifn 3895	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
217	216	ad3antlr 722	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) ∧ (𝑓‘𝑖) < (𝐴‘𝑖)) → ¬ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))
218	215, 217	pm2.65da 851	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ¬ (𝑓‘𝑖) < (𝐴‘𝑖))
219	155, 158, 69	syl2anc 579	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ∈ ℝ)
220	219, 167	lenltd 10437	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → ((𝐴‘𝑖) ≤ (𝑓‘𝑖) ↔ ¬ (𝑓‘𝑖) < (𝐴‘𝑖)))
221	218, 220	mpbird 248	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝐴‘𝑖) ≤ (𝑓‘𝑖))
222	18	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → -∞ ∈ ℝ^*)
223	84	adantlr 706	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝐵‘𝑖) ∈ ℝ^*)
224		iooltub 40307	. . . . . . . . . . . . 13 ⊢ ((-∞ ∈ ℝ^* ∧ (𝐵‘𝑖) ∈ ℝ^* ∧ (𝑓‘𝑖) ∈ (-∞(,)(𝐵‘𝑖))) → (𝑓‘𝑖) < (𝐵‘𝑖))
225	222, 223, 165, 224	syl3anc 1490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑓 ∈ (𝑖(𝐻‘𝑋)(𝐵‘𝑖))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
226	155, 157, 158, 225	syl21anc 866	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) < (𝐵‘𝑖))
227	153, 154, 168, 221, 226	elicod 12426	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑓 ∈ ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
228	145, 151, 152, 227	syl21anc 866	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) ∧ 𝑖 ∈ 𝑋) → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
229	228	ex 401	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑖 ∈ 𝑋 → (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
230	144, 229	ralrimi 3104	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
231	141, 230	jca 507	. . . . . 6 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → (𝑓 Fn 𝑋 ∧ ∀𝑖 ∈ 𝑋 (𝑓‘𝑖) ∈ ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
232	231, 86	sylibr 225	. . . . 5 ⊢ ((𝜑 ∧ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)))
233	232	ex 401	. . . 4 ⊢ (𝜑 → (𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) → 𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖))))
234	109, 233	impbid 203	. . 3 ⊢ (𝜑 → (𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
235	234	alrimiv 2022	. 2 ⊢ (𝜑 → ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
236		dfcleq 2759	. 2 ⊢ (X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))) ↔ ∀𝑓(𝑓 ∈ X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) ↔ 𝑓 ∈ ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖)))))
237	235, 236	sylibr 225	1 ⊢ (𝜑 → X𝑖 ∈ 𝑋 ((𝐴‘𝑖)[,)(𝐵‘𝑖)) = ∩ 𝑖 ∈ 𝑋 ((𝑖(𝐻‘𝑋)(𝐵‘𝑖)) ∖ (𝑖(𝐻‘𝑋)(𝐴‘𝑖))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 197 ∧ wa 384 ∀wal 1650 = wceq 1652 ∃wex 1874 ∈ wcel 2155 ≠ wne 2937 ∀wral 3055 Vcvv 3350 ∖ cdif 3729 ⊆ wss 3732 ∅c0 4079 ifcif 4243 ∩ ciin 4677 class class class wbr 4809 ↦ cmpt 4888 Fn wfn 6063 ⟶wf 6064 ‘cfv 6068 (class class class)co 6842 ↦ cmpt2 6844 Xcixp 8113 Fincfn 8160 ℝcr 10188 -∞cmnf 10326 ℝ^*cxr 10327 < clt 10328 ≤ cle 10329 (,)cioo 12377 [,)cico 12379

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1890 ax-4 1904 ax-5 2005 ax-6 2070 ax-7 2105 ax-8 2157 ax-9 2164 ax-10 2183 ax-11 2198 ax-12 2211 ax-13 2352 ax-ext 2743 ax-rep 4930 ax-sep 4941 ax-nul 4949 ax-pow 5001 ax-pr 5062 ax-un 7147 ax-cnex 10245 ax-resscn 10246 ax-pre-lttri 10263 ax-pre-lttrn 10264

This theorem depends on definitions: df-bi 198 df-an 385 df-or 874 df-3or 1108 df-3an 1109 df-tru 1656 df-ex 1875 df-nf 1879 df-sb 2063 df-mo 2565 df-eu 2582 df-clab 2752 df-cleq 2758 df-clel 2761 df-nfc 2896 df-ne 2938 df-nel 3041 df-ral 3060 df-rex 3061 df-reu 3062 df-rab 3064 df-v 3352 df-sbc 3597 df-csb 3692 df-dif 3735 df-un 3737 df-in 3739 df-ss 3746 df-nul 4080 df-if 4244 df-pw 4317 df-sn 4335 df-pr 4337 df-op 4341 df-uni 4595 df-iun 4678 df-iin 4679 df-br 4810 df-opab 4872 df-mpt 4889 df-id 5185 df-po 5198 df-so 5199 df-xp 5283 df-rel 5284 df-cnv 5285 df-co 5286 df-dm 5287 df-rn 5288 df-res 5289 df-ima 5290 df-iota 6031 df-fun 6070 df-fn 6071 df-f 6072 df-f1 6073 df-fo 6074 df-f1o 6075 df-fv 6076 df-ov 6845 df-oprab 6846 df-mpt2 6847 df-1st 7366 df-2nd 7367 df-er 7947 df-ixp 8114 df-en 8161 df-dom 8162 df-sdom 8163 df-pnf 10330 df-mnf 10331 df-xr 10332 df-ltxr 10333 df-le 10334 df-ioo 12381 df-ico 12383

This theorem is referenced by: hoimbllem 41416

W3C validator