Users' Mathboxes 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.
StepHypRef Expression
1 nfv 2009 . . . . . . . 8 𝑖𝜑
2 nfcv 2907 . . . . . . . . 9 𝑖𝑓
3 nfixp1 8133 . . . . . . . . 9 𝑖X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))
42, 3nfel 2920 . . . . . . . 8 𝑖 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))
51, 4nfan 1998 . . . . . . 7 𝑖(𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)))
6 ixpfn 8119 . . . . . . . . . . . . 13 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → 𝑓 Fn 𝑋)
76ad2antlr 718 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 Fn 𝑋)
8 fveq2 6375 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝐵𝑘) = (𝐵𝑖))
98oveq2d 6858 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) = (-∞(,)(𝐵𝑖)))
10 iftrue 4249 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) = (-∞(,)(𝐵𝑖)))
119, 10eqtr4d 2802 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
12 eqimss 3817 . . . . . . . . . . . . . . . . 17 ((-∞(,)(𝐵𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) → (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
1311, 12syl 17 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
14 ioossre 12437 . . . . . . . . . . . . . . . . 17 (-∞(,)(𝐵𝑘)) ⊆ ℝ
15 iffalse 4252 . . . . . . . . . . . . . . . . 17 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) = ℝ)
1614, 15syl5sseqr 3814 . . . . . . . . . . . . . . . 16 𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
1713, 16pm2.61i 176 . . . . . . . . . . . . . . 15 (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ)
18 mnfxr 10350 . . . . . . . . . . . . . . . . 17 -∞ ∈ ℝ*
1918a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → -∞ ∈ ℝ*)
20 hspdifhsp.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵:𝑋⟶ℝ)
2120ffvelrnda 6549 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
2221rexrd 10343 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ*)
2322adantlr 706 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝐵𝑘) ∈ ℝ*)
24 hspdifhsp.a . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴:𝑋⟶ℝ)
2524ffvelrnda 6549 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ)
26 icossre 12456 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ*) → ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ ℝ)
2725, 22, 26syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑋) → ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ ℝ)
2827adantlr 706 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ ℝ)
29 simpl 474 . . . . . . . . . . . . . . . . . . 19 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)))
30 simpr 477 . . . . . . . . . . . . . . . . . . 19 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → 𝑘𝑋)
31 fveq2 6375 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → (𝐴𝑖) = (𝐴𝑘))
32 fveq2 6375 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → (𝐵𝑖) = (𝐵𝑘))
3331, 32oveq12d 6860 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑘 → ((𝐴𝑖)[,)(𝐵𝑖)) = ((𝐴𝑘)[,)(𝐵𝑘)))
3433fvixp 8118 . . . . . . . . . . . . . . . . . . 19 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
3529, 30, 34syl2anc 579 . . . . . . . . . . . . . . . . . 18 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
3635adantll 705 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
3728, 36sseldd 3762 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
3837mnfltd 12158 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → -∞ < (𝑓𝑘))
3925rexrd 10343 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ*)
4039adantlr 706 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝐴𝑘) ∈ ℝ*)
41 icoltub 40305 . . . . . . . . . . . . . . . . 17 (((𝐴𝑘) ∈ ℝ* ∧ (𝐵𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑓𝑘) < (𝐵𝑘))
4240, 23, 36, 41syl3anc 1490 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) < (𝐵𝑘))
4319, 23, 37, 38, 42eliood 40294 . . . . . . . . . . . . . . 15 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (-∞(,)(𝐵𝑘)))
4417, 43sseldi 3759 . . . . . . . . . . . . . 14 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
4544adantlr 706 . . . . . . . . . . . . 13 ((((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
4645ralrimiva 3113 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
477, 46jca 507 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ)))
48 vex 3353 . . . . . . . . . . . 12 𝑓 ∈ V
4948elixp 8120 . . . . . . . . . . 11 (𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ)))
5047, 49sylibr 225 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
51 hspdifhsp.h . . . . . . . . . . . . 13 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52 equequ1 2122 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑘 → (𝑖 = 𝑙𝑘 = 𝑙))
5352ifbid 4265 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑘 → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
5453cbvixpv 8131 . . . . . . . . . . . . . . . 16 X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)
5554a1i 11 . . . . . . . . . . . . . . 15 ((𝑙𝑥𝑦 ∈ ℝ) → X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
5655mpt2eq3ia 6918 . . . . . . . . . . . . . 14 (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
5756mpteq2i 4900 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
5851, 57eqtri 2787 . . . . . . . . . . . 12 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
59 hspdifhsp.x . . . . . . . . . . . . 13 (𝜑𝑋 ∈ Fin)
6059adantr 472 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝑋 ∈ Fin)
61 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝑖𝑋)
6220adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → 𝐵:𝑋⟶ℝ)
6362, 61ffvelrnd 6550 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
6458, 60, 61, 63hspval 41395 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝑖(𝐻𝑋)(𝐵𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
6564adantlr 706 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑖(𝐻𝑋)(𝐵𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
6650, 65eleqtrrd 2847 . . . . . . . . 9 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
6718a1i 11 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → -∞ ∈ ℝ*)
6824adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐴:𝑋⟶ℝ)
6968, 61ffvelrnd 6550 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
7069rexrd 10343 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
7170adantr 472 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝐴𝑖) ∈ ℝ*)
72 simpr 477 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
7358, 60, 61, 69hspval 41395 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝑖(𝐻𝑋)(𝐴𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
7473adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑖(𝐻𝑋)(𝐴𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
7572, 74eleqtrd 2846 . . . . . . . . . . . . 13 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
7661adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑖𝑋)
77 iftrue 4249 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = (-∞(,)(𝐴𝑖)))
7877fvixp 8118 . . . . . . . . . . . . 13 ((𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
7975, 76, 78syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
80 iooltub 40307 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ (𝐴𝑖) ∈ ℝ* ∧ (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖))) → (𝑓𝑖) < (𝐴𝑖))
8167, 71, 79, 80syl3anc 1490 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑓𝑖) < (𝐴𝑖))
8281adantllr 710 . . . . . . . . . 10 ((((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑓𝑖) < (𝐴𝑖))
8370adantlr 706 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
8463rexrd 10343 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
8584adantlr 706 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
8648elixp 8120 . . . . . . . . . . . . . . . . 17 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
8786biimpi 207 . . . . . . . . . . . . . . . 16 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
8887simprd 489 . . . . . . . . . . . . . . 15 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
89 rspa 3077 . . . . . . . . . . . . . . 15 ((∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
9088, 89sylan 575 . . . . . . . . . . . . . 14 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
9190adantll 705 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
92 icogelb 12427 . . . . . . . . . . . . 13 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))) → (𝐴𝑖) ≤ (𝑓𝑖))
9383, 85, 91, 92syl3anc 1490 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐴𝑖) ≤ (𝑓𝑖))
9469adantlr 706 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
95 icossre 12456 . . . . . . . . . . . . . . . 16 (((𝐴𝑖) ∈ ℝ ∧ (𝐵𝑖) ∈ ℝ*) → ((𝐴𝑖)[,)(𝐵𝑖)) ⊆ ℝ)
9669, 84, 95syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → ((𝐴𝑖)[,)(𝐵𝑖)) ⊆ ℝ)
9796adantlr 706 . . . . . . . . . . . . . 14 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ((𝐴𝑖)[,)(𝐵𝑖)) ⊆ ℝ)
9897, 91sseldd 3762 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ)
9994, 98lenltd 10437 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ((𝐴𝑖) ≤ (𝑓𝑖) ↔ ¬ (𝑓𝑖) < (𝐴𝑖)))
10093, 99mpbid 223 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ¬ (𝑓𝑖) < (𝐴𝑖))
101100adantr 472 . . . . . . . . . 10 ((((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → ¬ (𝑓𝑖) < (𝐴𝑖))
10282, 101pm2.65da 851 . . . . . . . . 9 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ¬ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
10366, 102eldifd 3743 . . . . . . . 8 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
104103ex 401 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) → (𝑖𝑋𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
1055, 104ralrimi 3104 . . . . . 6 ((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) → ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
106 eliin 4681 . . . . . . 7 (𝑓 ∈ V → (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
10748, 106ax-mp 5 . . . . . 6 (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
108105, 107sylibr 225 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) → 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
109108ex 401 . . . 4 (𝜑 → (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
110 hspdifhsp.n . . . . . . . . . 10 (𝜑𝑋 ≠ ∅)
111 n0 4095 . . . . . . . . . . 11 (𝑋 ≠ ∅ ↔ ∃𝑘 𝑘𝑋)
112111biimpi 207 . . . . . . . . . 10 (𝑋 ≠ ∅ → ∃𝑘 𝑘𝑋)
113110, 112syl 17 . . . . . . . . 9 (𝜑 → ∃𝑘 𝑘𝑋)
114113adantr 472 . . . . . . . 8 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → ∃𝑘 𝑘𝑋)
115 simpl 474 . . . . . . . . . . . . . . 15 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
116 simpr 477 . . . . . . . . . . . . . . 15 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑘𝑋)
117 id 22 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑘𝑖 = 𝑘)
118117, 32oveq12d 6860 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑘 → (𝑖(𝐻𝑋)(𝐵𝑖)) = (𝑘(𝐻𝑋)(𝐵𝑘)))
119117, 31oveq12d 6860 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑘 → (𝑖(𝐻𝑋)(𝐴𝑖)) = (𝑘(𝐻𝑋)(𝐴𝑘)))
120118, 119difeq12d 3891 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) = ((𝑘(𝐻𝑋)(𝐵𝑘)) ∖ (𝑘(𝐻𝑋)(𝐴𝑘))))
121120eleq2d 2830 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ 𝑓 ∈ ((𝑘(𝐻𝑋)(𝐵𝑘)) ∖ (𝑘(𝐻𝑋)(𝐴𝑘)))))
122115, 116, 121eliind 39823 . . . . . . . . . . . . . 14 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑓 ∈ ((𝑘(𝐻𝑋)(𝐵𝑘)) ∖ (𝑘(𝐻𝑋)(𝐴𝑘))))
123122eldifad 3744 . . . . . . . . . . . . 13 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑓 ∈ (𝑘(𝐻𝑋)(𝐵𝑘)))
124123adantll 705 . . . . . . . . . . . 12 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑓 ∈ (𝑘(𝐻𝑋)(𝐵𝑘)))
125 equequ1 2122 . . . . . . . . . . . . . . . . . . 19 (𝑖 = → (𝑖 = 𝑙 = 𝑙))
126125ifbid 4265 . . . . . . . . . . . . . . . . . 18 (𝑖 = → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if( = 𝑙, (-∞(,)𝑦), ℝ))
127126cbvixpv 8131 . . . . . . . . . . . . . . . . 17 X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ)
128127a1i 11 . . . . . . . . . . . . . . . 16 ((𝑙𝑥𝑦 ∈ ℝ) → X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ))
129128mpt2eq3ia 6918 . . . . . . . . . . . . . . 15 (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ))
130129mpteq2i 4900 . . . . . . . . . . . . . 14 (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ)))
13151, 130eqtri 2787 . . . . . . . . . . . . 13 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ)))
13259ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑋 ∈ Fin)
133 simpr 477 . . . . . . . . . . . . 13 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑘𝑋)
13421adantlr 706 . . . . . . . . . . . . 13 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
135131, 132, 133, 134hspval 41395 . . . . . . . . . . . 12 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → (𝑘(𝐻𝑋)(𝐵𝑘)) = X𝑋 if( = 𝑘, (-∞(,)(𝐵𝑘)), ℝ))
136124, 135eleqtrd 2846 . . . . . . . . . . 11 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑓X𝑋 if( = 𝑘, (-∞(,)(𝐵𝑘)), ℝ))
137 ixpfn 8119 . . . . . . . . . . 11 (𝑓X𝑋 if( = 𝑘, (-∞(,)(𝐵𝑘)), ℝ) → 𝑓 Fn 𝑋)
138136, 137syl 17 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑓 Fn 𝑋)
139138ex 401 . . . . . . . . 9 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝑘𝑋𝑓 Fn 𝑋))
140139exlimdv 2028 . . . . . . . 8 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (∃𝑘 𝑘𝑋𝑓 Fn 𝑋))
141114, 140mpd 15 . . . . . . 7 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝑓 Fn 𝑋)
142 nfii1 4707 . . . . . . . . . 10 𝑖 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))
1432, 142nfel 2920 . . . . . . . . 9 𝑖 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))
1441, 143nfan 1998 . . . . . . . 8 𝑖(𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
145 simpll 783 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝜑)
146107biimpi 207 . . . . . . . . . . . . 13 (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
147146adantr 472 . . . . . . . . . . . 12 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
148 simpr 477 . . . . . . . . . . . 12 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → 𝑖𝑋)
149 rspa 3077 . . . . . . . . . . . 12 ((∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
150147, 148, 149syl2anc 579 . . . . . . . . . . 11 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
151150adantll 705 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
152 simpr 477 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑖𝑋)
15370adantlr 706 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
15484adantlr 706 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
155 simpll 783 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝜑)
156 eldifi 3894 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
157156ad2antlr 718 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
158 simpr 477 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑖𝑋)
159 ioossre 12437 . . . . . . . . . . . . . 14 (-∞(,)(𝐵𝑖)) ⊆ ℝ
160 simplr 785 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
16164adantlr 706 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑖(𝐻𝑋)(𝐵𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
162160, 161eleqtrd 2846 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
163 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑖𝑋)
16410fvixp 8118 . . . . . . . . . . . . . . 15 ((𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ (-∞(,)(𝐵𝑖)))
165162, 163, 164syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ (-∞(,)(𝐵𝑖)))
166159, 165sseldi 3759 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ)
167155, 157, 158, 166syl21anc 866 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ)
168167rexrd 10343 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ*)
169 simpl 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝜑)
170156adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
171169, 170jca 507 . . . . . . . . . . . . . . 15 ((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))))
172171ad2antrr 717 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))))
173 simplr 785 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑖𝑋)
174 simpr 477 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) < (𝐴𝑖))
175 ixpfn 8119 . . . . . . . . . . . . . . . . . . 19 (𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) → 𝑓 Fn 𝑋)
176162, 175syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 Fn 𝑋)
177176adantr 472 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓 Fn 𝑋)
178 fveq2 6375 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → (𝑓𝑘) = (𝑓𝑖))
179178adantl 473 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘 = 𝑖) → (𝑓𝑘) = (𝑓𝑖))
18018a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → -∞ ∈ ℝ*)
18170ad4ant13 757 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝐴𝑖) ∈ ℝ*)
182166adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) ∈ ℝ)
183182mnfltd 12158 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → -∞ < (𝑓𝑖))
184 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) < (𝐴𝑖))
185180, 181, 182, 183, 184eliood 40294 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
186185adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘 = 𝑖) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
187179, 186eqeltrd 2844 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘 = 𝑖) → (𝑓𝑘) ∈ (-∞(,)(𝐴𝑖)))
188187adantlr 706 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ 𝑘 = 𝑖) → (𝑓𝑘) ∈ (-∞(,)(𝐴𝑖)))
18977eqcomd 2771 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (-∞(,)(𝐴𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
190189adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ 𝑘 = 𝑖) → (-∞(,)(𝐴𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
191188, 190eleqtrd 2846 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ 𝑘 = 𝑖) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
19210, 159syl6eqss 3815 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ⊆ ℝ)
193 ssid 3783 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℝ
19415, 193syl6eqss 3815 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ⊆ ℝ)
195192, 194pm2.61i 176 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ⊆ ℝ
196162adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
197 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → 𝑘𝑋)
198 fvixp2 39967 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
199196, 197, 198syl2anc 579 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
200195, 199sseldi 3759 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
201200adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓𝑘) ∈ ℝ)
202 iffalse 4252 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = ℝ)
203202eqcomd 2771 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 = 𝑖 → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
204203adantl 473 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
205201, 204eleqtrd 2846 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
206205adantllr 710 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
207191, 206pm2.61dan 847 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
208207ralrimiva 3113 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
209177, 208jca 507 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ)))
21048elixp 8120 . . . . . . . . . . . . . . . 16 (𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ)))
211209, 210sylibr 225 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
21273eqcomd 2771 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = (𝑖(𝐻𝑋)(𝐴𝑖)))
213212ad4ant13 757 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = (𝑖(𝐻𝑋)(𝐴𝑖)))
214211, 213eleqtrd 2846 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
215172, 173, 174, 214syl21anc 866 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
216 eldifn 3895 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → ¬ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
217216ad3antlr 722 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → ¬ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
218215, 217pm2.65da 851 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → ¬ (𝑓𝑖) < (𝐴𝑖))
219155, 158, 69syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
220219, 167lenltd 10437 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → ((𝐴𝑖) ≤ (𝑓𝑖) ↔ ¬ (𝑓𝑖) < (𝐴𝑖)))
221218, 220mpbird 248 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐴𝑖) ≤ (𝑓𝑖))
22218a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → -∞ ∈ ℝ*)
22384adantlr 706 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
224 iooltub 40307 . . . . . . . . . . . . 13 ((-∞ ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝑓𝑖) ∈ (-∞(,)(𝐵𝑖))) → (𝑓𝑖) < (𝐵𝑖))
225222, 223, 165, 224syl3anc 1490 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) < (𝐵𝑖))
226155, 157, 158, 225syl21anc 866 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) < (𝐵𝑖))
227153, 154, 168, 221, 226elicod 12426 . . . . . . . . . 10 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
228145, 151, 152, 227syl21anc 866 . . . . . . . . 9 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
229228ex 401 . . . . . . . 8 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝑖𝑋 → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
230144, 229ralrimi 3104 . . . . . . 7 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
231141, 230jca 507 . . . . . 6 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝑓 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
232231, 86sylibr 225 . . . . 5 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)))
233232ex 401 . . . 4 (𝜑 → (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))))
234109, 233impbid 203 . . 3 (𝜑 → (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
235234alrimiv 2022 . 2 (𝜑 → ∀𝑓(𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
236 dfcleq 2759 . 2 (X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) = 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ ∀𝑓(𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
237235, 236sylibr 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
  Copyright terms: Public domain W3C validator