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 39303
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 1829 . . . . . . . 8 𝑖𝜑
2 nfcv 2750 . . . . . . . . 9 𝑖𝑓
3 nfixp1 7791 . . . . . . . . 9 𝑖X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))
42, 3nfel 2762 . . . . . . . 8 𝑖 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))
51, 4nfan 1815 . . . . . . 7 𝑖(𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)))
6 ixpfn 7777 . . . . . . . . . . . . 13 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → 𝑓 Fn 𝑋)
76ad2antlr 758 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 Fn 𝑋)
8 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 𝑖 → (𝐵𝑘) = (𝐵𝑖))
98oveq2d 6543 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) = (-∞(,)(𝐵𝑖)))
10 iftrue 4041 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) = (-∞(,)(𝐵𝑖)))
119, 10eqtr4d 2646 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
12 eqimss 3619 . . . . . . . . . . . . . . . . 17 ((-∞(,)(𝐵𝑘)) = if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) → (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
1311, 12syl 17 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
14 ioossre 12062 . . . . . . . . . . . . . . . . 17 (-∞(,)(𝐵𝑘)) ⊆ ℝ
15 iffalse 4044 . . . . . . . . . . . . . . . . 17 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) = ℝ)
1614, 15syl5sseqr 3616 . . . . . . . . . . . . . . . 16 𝑘 = 𝑖 → (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
1713, 16pm2.61i 174 . . . . . . . . . . . . . . 15 (-∞(,)(𝐵𝑘)) ⊆ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ)
18 mnfxr 11783 . . . . . . . . . . . . . . . . 17 -∞ ∈ ℝ*
1918a1i 11 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → -∞ ∈ ℝ*)
20 hspdifhsp.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵:𝑋⟶ℝ)
2120ffvelrnda 6252 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
2221rexrd 9945 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝑋) → (𝐵𝑘) ∈ ℝ*)
2322adantlr 746 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝐵𝑘) ∈ ℝ*)
24 hspdifhsp.a . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴:𝑋⟶ℝ)
2524ffvelrnda 6252 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ)
26 icossre 12081 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ*) → ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ ℝ)
2725, 22, 26syl2anc 690 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑋) → ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ ℝ)
2827adantlr 746 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → ((𝐴𝑘)[,)(𝐵𝑘)) ⊆ ℝ)
29 simpl 471 . . . . . . . . . . . . . . . . . . 19 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)))
30 simpr 475 . . . . . . . . . . . . . . . . . . 19 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → 𝑘𝑋)
31 fveq2 6088 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → (𝐴𝑖) = (𝐴𝑘))
32 fveq2 6088 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → (𝐵𝑖) = (𝐵𝑘))
3331, 32oveq12d 6545 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑘 → ((𝐴𝑖)[,)(𝐵𝑖)) = ((𝐴𝑘)[,)(𝐵𝑘)))
3433fvixp 7776 . . . . . . . . . . . . . . . . . . 19 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
3529, 30, 34syl2anc 690 . . . . . . . . . . . . . . . . . 18 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
3635adantll 745 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘)))
3728, 36sseldd 3568 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
3837mnfltd 11795 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → -∞ < (𝑓𝑘))
3925rexrd 9945 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝑋) → (𝐴𝑘) ∈ ℝ*)
4039adantlr 746 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝐴𝑘) ∈ ℝ*)
41 icoltub 38376 . . . . . . . . . . . . . . . . 17 (((𝐴𝑘) ∈ ℝ* ∧ (𝐵𝑘) ∈ ℝ* ∧ (𝑓𝑘) ∈ ((𝐴𝑘)[,)(𝐵𝑘))) → (𝑓𝑘) < (𝐵𝑘))
4240, 23, 36, 41syl3anc 1317 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) < (𝐵𝑘))
4319, 23, 37, 38, 42eliood 38364 . . . . . . . . . . . . . . 15 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ (-∞(,)(𝐵𝑘)))
4417, 43sseldi 3565 . . . . . . . . . . . . . 14 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
4544adantlr 746 . . . . . . . . . . . . 13 ((((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
4645ralrimiva 2948 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
477, 46jca 552 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ)))
48 vex 3175 . . . . . . . . . . . 12 𝑓 ∈ V
4948elixp 7778 . . . . . . . . . . 11 (𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ)))
5047, 49sylibr 222 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
51 hspdifhsp.h . . . . . . . . . . . . 13 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)))
52 equequ1 1938 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑘 → (𝑖 = 𝑙𝑘 = 𝑙))
5352ifbid 4057 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑘 → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
5453cbvixpv 7789 . . . . . . . . . . . . . . . 16 X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)
5554a1i 11 . . . . . . . . . . . . . . 15 ((𝑙𝑥𝑦 ∈ ℝ) → X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
5655mpt2eq3ia 6596 . . . . . . . . . . . . . 14 (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ))
5756mpteq2i 4663 . . . . . . . . . . . . 13 (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
5851, 57eqtri 2631 . . . . . . . . . . . 12 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑘𝑥 if(𝑘 = 𝑙, (-∞(,)𝑦), ℝ)))
59 hspdifhsp.x . . . . . . . . . . . . 13 (𝜑𝑋 ∈ Fin)
6059adantr 479 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝑋 ∈ Fin)
61 simpr 475 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → 𝑖𝑋)
6220adantr 479 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → 𝐵:𝑋⟶ℝ)
6362, 61ffvelrnd 6253 . . . . . . . . . . . 12 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ)
6458, 60, 61, 63hspval 39296 . . . . . . . . . . 11 ((𝜑𝑖𝑋) → (𝑖(𝐻𝑋)(𝐵𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
6564adantlr 746 . . . . . . . . . 10 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑖(𝐻𝑋)(𝐵𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
6650, 65eleqtrrd 2690 . . . . . . . . 9 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
6718a1i 11 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → -∞ ∈ ℝ*)
6824adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → 𝐴:𝑋⟶ℝ)
6968, 61ffvelrnd 6253 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
7069rexrd 9945 . . . . . . . . . . . . 13 ((𝜑𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
7170adantr 479 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝐴𝑖) ∈ ℝ*)
72 simpr 475 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
7358, 60, 61, 69hspval 39296 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → (𝑖(𝐻𝑋)(𝐴𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
7473adantr 479 . . . . . . . . . . . . . 14 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑖(𝐻𝑋)(𝐴𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
7572, 74eleqtrd 2689 . . . . . . . . . . . . 13 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
7661adantr 479 . . . . . . . . . . . . 13 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑖𝑋)
77 iftrue 4041 . . . . . . . . . . . . . 14 (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = (-∞(,)(𝐴𝑖)))
7877fvixp 7776 . . . . . . . . . . . . 13 ((𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
7975, 76, 78syl2anc 690 . . . . . . . . . . . 12 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
80 iooltub 38379 . . . . . . . . . . . 12 ((-∞ ∈ ℝ* ∧ (𝐴𝑖) ∈ ℝ* ∧ (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖))) → (𝑓𝑖) < (𝐴𝑖))
8167, 71, 79, 80syl3anc 1317 . . . . . . . . . . 11 (((𝜑𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑓𝑖) < (𝐴𝑖))
8281adantllr 750 . . . . . . . . . 10 ((((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → (𝑓𝑖) < (𝐴𝑖))
8370adantlr 746 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
8463rexrd 9945 . . . . . . . . . . . . . 14 ((𝜑𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
8584adantlr 746 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
8648elixp 7778 . . . . . . . . . . . . . . . . 17 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
8786biimpi 204 . . . . . . . . . . . . . . . 16 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
8887simprd 477 . . . . . . . . . . . . . . 15 (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
89 rspa 2913 . . . . . . . . . . . . . . 15 ((∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
9088, 89sylan 486 . . . . . . . . . . . . . 14 ((𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
9190adantll 745 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
92 icogelb 12052 . . . . . . . . . . . . 13 (((𝐴𝑖) ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))) → (𝐴𝑖) ≤ (𝑓𝑖))
9383, 85, 91, 92syl3anc 1317 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐴𝑖) ≤ (𝑓𝑖))
9469adantlr 746 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
95 icossre 12081 . . . . . . . . . . . . . . . 16 (((𝐴𝑖) ∈ ℝ ∧ (𝐵𝑖) ∈ ℝ*) → ((𝐴𝑖)[,)(𝐵𝑖)) ⊆ ℝ)
9669, 84, 95syl2anc 690 . . . . . . . . . . . . . . 15 ((𝜑𝑖𝑋) → ((𝐴𝑖)[,)(𝐵𝑖)) ⊆ ℝ)
9796adantlr 746 . . . . . . . . . . . . . 14 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ((𝐴𝑖)[,)(𝐵𝑖)) ⊆ ℝ)
9897, 91sseldd 3568 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ)
9994, 98lenltd 10034 . . . . . . . . . . . 12 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ((𝐴𝑖) ≤ (𝑓𝑖) ↔ ¬ (𝑓𝑖) < (𝐴𝑖)))
10093, 99mpbid 220 . . . . . . . . . . 11 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ¬ (𝑓𝑖) < (𝐴𝑖))
101100adantr 479 . . . . . . . . . 10 ((((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖))) → ¬ (𝑓𝑖) < (𝐴𝑖))
10282, 101pm2.65da 597 . . . . . . . . 9 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → ¬ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
10366, 102eldifd 3550 . . . . . . . 8 (((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
104103ex 448 . . . . . . 7 ((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) → (𝑖𝑋𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
1055, 104ralrimi 2939 . . . . . 6 ((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) → ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
106 eliin 4455 . . . . . . 7 (𝑓 ∈ V → (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
10748, 106ax-mp 5 . . . . . 6 (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
108105, 107sylibr 222 . . . . 5 ((𝜑𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))) → 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
109108ex 448 . . . 4 (𝜑 → (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) → 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
110 hspdifhsp.n . . . . . . . . . 10 (𝜑𝑋 ≠ ∅)
111 n0 3889 . . . . . . . . . . 11 (𝑋 ≠ ∅ ↔ ∃𝑘 𝑘𝑋)
112111biimpi 204 . . . . . . . . . 10 (𝑋 ≠ ∅ → ∃𝑘 𝑘𝑋)
113110, 112syl 17 . . . . . . . . 9 (𝜑 → ∃𝑘 𝑘𝑋)
114113adantr 479 . . . . . . . 8 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → ∃𝑘 𝑘𝑋)
115 simpl 471 . . . . . . . . . . . . . . 15 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
116 simpr 475 . . . . . . . . . . . . . . 15 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑘𝑋)
117 id 22 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑘𝑖 = 𝑘)
118117, 32oveq12d 6545 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑘 → (𝑖(𝐻𝑋)(𝐵𝑖)) = (𝑘(𝐻𝑋)(𝐵𝑘)))
119117, 31oveq12d 6545 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑘 → (𝑖(𝐻𝑋)(𝐴𝑖)) = (𝑘(𝐻𝑋)(𝐴𝑘)))
120118, 119difeq12d 3690 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) = ((𝑘(𝐻𝑋)(𝐵𝑘)) ∖ (𝑘(𝐻𝑋)(𝐴𝑘))))
121120eleq2d 2672 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → (𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ 𝑓 ∈ ((𝑘(𝐻𝑋)(𝐵𝑘)) ∖ (𝑘(𝐻𝑋)(𝐴𝑘)))))
122115, 116, 121eliind 38062 . . . . . . . . . . . . . 14 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑓 ∈ ((𝑘(𝐻𝑋)(𝐵𝑘)) ∖ (𝑘(𝐻𝑋)(𝐴𝑘))))
123122eldifad 3551 . . . . . . . . . . . . 13 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑘𝑋) → 𝑓 ∈ (𝑘(𝐻𝑋)(𝐵𝑘)))
124123adantll 745 . . . . . . . . . . . 12 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑓 ∈ (𝑘(𝐻𝑋)(𝐵𝑘)))
125 equequ1 1938 . . . . . . . . . . . . . . . . . . 19 (𝑖 = → (𝑖 = 𝑙 = 𝑙))
126125ifbid 4057 . . . . . . . . . . . . . . . . . 18 (𝑖 = → if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = if( = 𝑙, (-∞(,)𝑦), ℝ))
127126cbvixpv 7789 . . . . . . . . . . . . . . . . 17 X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ)
128127a1i 11 . . . . . . . . . . . . . . . 16 ((𝑙𝑥𝑦 ∈ ℝ) → X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ) = X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ))
129128mpt2eq3ia 6596 . . . . . . . . . . . . . . 15 (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ)) = (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ))
130129mpteq2i 4663 . . . . . . . . . . . . . 14 (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑖𝑥 if(𝑖 = 𝑙, (-∞(,)𝑦), ℝ))) = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ)))
13151, 130eqtri 2631 . . . . . . . . . . . . 13 𝐻 = (𝑥 ∈ Fin ↦ (𝑙𝑥, 𝑦 ∈ ℝ ↦ X𝑥 if( = 𝑙, (-∞(,)𝑦), ℝ)))
13259ad2antrr 757 . . . . . . . . . . . . 13 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑋 ∈ Fin)
133 simpr 475 . . . . . . . . . . . . 13 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑘𝑋)
13421adantlr 746 . . . . . . . . . . . . 13 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → (𝐵𝑘) ∈ ℝ)
135131, 132, 133, 134hspval 39296 . . . . . . . . . . . 12 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → (𝑘(𝐻𝑋)(𝐵𝑘)) = X𝑋 if( = 𝑘, (-∞(,)(𝐵𝑘)), ℝ))
136124, 135eleqtrd 2689 . . . . . . . . . . 11 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑓X𝑋 if( = 𝑘, (-∞(,)(𝐵𝑘)), ℝ))
137 ixpfn 7777 . . . . . . . . . . 11 (𝑓X𝑋 if( = 𝑘, (-∞(,)(𝐵𝑘)), ℝ) → 𝑓 Fn 𝑋)
138136, 137syl 17 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑘𝑋) → 𝑓 Fn 𝑋)
139138ex 448 . . . . . . . . 9 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝑘𝑋𝑓 Fn 𝑋))
140139exlimdv 1847 . . . . . . . 8 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (∃𝑘 𝑘𝑋𝑓 Fn 𝑋))
141114, 140mpd 15 . . . . . . 7 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝑓 Fn 𝑋)
142 nfii1 4481 . . . . . . . . . 10 𝑖 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))
1432, 142nfel 2762 . . . . . . . . 9 𝑖 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))
1441, 143nfan 1815 . . . . . . . 8 𝑖(𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
145 simpll 785 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝜑)
146107biimpi 204 . . . . . . . . . . . . 13 (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
147146adantr 479 . . . . . . . . . . . 12 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → ∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
148 simpr 475 . . . . . . . . . . . 12 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → 𝑖𝑋)
149 rspa 2913 . . . . . . . . . . . 12 ((∀𝑖𝑋 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
150147, 148, 149syl2anc 690 . . . . . . . . . . 11 ((𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
151150adantll 745 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
152 simpr 475 . . . . . . . . . 10 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑖𝑋)
15370adantlr 746 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ*)
15484adantlr 746 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
155 simpll 785 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝜑)
156 eldifi 3693 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
157156ad2antlr 758 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
158 simpr 475 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → 𝑖𝑋)
159 ioossre 12062 . . . . . . . . . . . . . 14 (-∞(,)(𝐵𝑖)) ⊆ ℝ
160 simplr 787 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
16164adantlr 746 . . . . . . . . . . . . . . . 16 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑖(𝐻𝑋)(𝐵𝑖)) = X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
162160, 161eleqtrd 2689 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
163 simpr 475 . . . . . . . . . . . . . . 15 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑖𝑋)
16410fvixp 7776 . . . . . . . . . . . . . . 15 ((𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ (-∞(,)(𝐵𝑖)))
165162, 163, 164syl2anc 690 . . . . . . . . . . . . . 14 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ (-∞(,)(𝐵𝑖)))
166159, 165sseldi 3565 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ)
167155, 157, 158, 166syl21anc 1316 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ)
168167rexrd 9945 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ℝ*)
169 simpl 471 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝜑)
170156adantl 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖)))
171169, 170jca 552 . . . . . . . . . . . . . . 15 ((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))))
172171ad2antrr 757 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))))
173 simplr 787 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑖𝑋)
174 simpr 475 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) < (𝐴𝑖))
175 ixpfn 7777 . . . . . . . . . . . . . . . . . . 19 (𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) → 𝑓 Fn 𝑋)
176162, 175syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → 𝑓 Fn 𝑋)
177176adantr 479 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓 Fn 𝑋)
178 fveq2 6088 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 = 𝑖 → (𝑓𝑘) = (𝑓𝑖))
179178adantl 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘 = 𝑖) → (𝑓𝑘) = (𝑓𝑖))
18018a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → -∞ ∈ ℝ*)
18170ad4ant13 1283 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝐴𝑖) ∈ ℝ*)
182166adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) ∈ ℝ)
183182mnfltd 11795 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → -∞ < (𝑓𝑖))
184 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) < (𝐴𝑖))
185180, 181, 182, 183, 184eliood 38364 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
186185adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘 = 𝑖) → (𝑓𝑖) ∈ (-∞(,)(𝐴𝑖)))
187179, 186eqeltrd 2687 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘 = 𝑖) → (𝑓𝑘) ∈ (-∞(,)(𝐴𝑖)))
188187adantlr 746 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ 𝑘 = 𝑖) → (𝑓𝑘) ∈ (-∞(,)(𝐴𝑖)))
18977eqcomd 2615 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 𝑖 → (-∞(,)(𝐴𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
190189adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ 𝑘 = 𝑖) → (-∞(,)(𝐴𝑖)) = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
191188, 190eleqtrd 2689 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ 𝑘 = 𝑖) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
19210, 159syl6eqss 3617 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ⊆ ℝ)
193 ssid 3586 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℝ ⊆ ℝ
19415, 193syl6eqss 3617 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ⊆ ℝ)
195192, 194pm2.61i 174 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ⊆ ℝ
196162adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
197 simpr 475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → 𝑘𝑋)
198 fvixp2 38180 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
199196, 197, 198syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐵𝑖)), ℝ))
200195, 199sseldi 3565 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ ℝ)
201200adantr 479 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓𝑘) ∈ ℝ)
202 iffalse 4044 . . . . . . . . . . . . . . . . . . . . . . 23 𝑘 = 𝑖 → if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = ℝ)
203202eqcomd 2615 . . . . . . . . . . . . . . . . . . . . . 22 𝑘 = 𝑖 → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
204203adantl 480 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → ℝ = if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
205201, 204eleqtrd 2689 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
206205adantllr 750 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) ∧ ¬ 𝑘 = 𝑖) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
207191, 206pm2.61dan 827 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) ∧ 𝑘𝑋) → (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
208207ralrimiva 2948 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
209177, 208jca 552 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ)))
21048elixp 7778 . . . . . . . . . . . . . . . 16 (𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) ↔ (𝑓 Fn 𝑋 ∧ ∀𝑘𝑋 (𝑓𝑘) ∈ if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ)))
211209, 210sylibr 222 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ))
21273eqcomd 2615 . . . . . . . . . . . . . . . 16 ((𝜑𝑖𝑋) → X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = (𝑖(𝐻𝑋)(𝐴𝑖)))
213212ad4ant13 1283 . . . . . . . . . . . . . . 15 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → X𝑘𝑋 if(𝑘 = 𝑖, (-∞(,)(𝐴𝑖)), ℝ) = (𝑖(𝐻𝑋)(𝐴𝑖)))
214211, 213eleqtrd 2689 . . . . . . . . . . . . . 14 ((((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
215172, 173, 174, 214syl21anc 1316 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
216 eldifn 3694 . . . . . . . . . . . . . 14 (𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → ¬ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
217216ad3antlr 762 . . . . . . . . . . . . 13 ((((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) ∧ (𝑓𝑖) < (𝐴𝑖)) → ¬ 𝑓 ∈ (𝑖(𝐻𝑋)(𝐴𝑖)))
218215, 217pm2.65da 597 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → ¬ (𝑓𝑖) < (𝐴𝑖))
219155, 158, 69syl2anc 690 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐴𝑖) ∈ ℝ)
220219, 167lenltd 10034 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → ((𝐴𝑖) ≤ (𝑓𝑖) ↔ ¬ (𝑓𝑖) < (𝐴𝑖)))
221218, 220mpbird 245 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝐴𝑖) ≤ (𝑓𝑖))
22218a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → -∞ ∈ ℝ*)
22384adantlr 746 . . . . . . . . . . . . 13 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝐵𝑖) ∈ ℝ*)
224 iooltub 38379 . . . . . . . . . . . . 13 ((-∞ ∈ ℝ* ∧ (𝐵𝑖) ∈ ℝ* ∧ (𝑓𝑖) ∈ (-∞(,)(𝐵𝑖))) → (𝑓𝑖) < (𝐵𝑖))
225222, 223, 165, 224syl3anc 1317 . . . . . . . . . . . 12 (((𝜑𝑓 ∈ (𝑖(𝐻𝑋)(𝐵𝑖))) ∧ 𝑖𝑋) → (𝑓𝑖) < (𝐵𝑖))
226155, 157, 158, 225syl21anc 1316 . . . . . . . . . . 11 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) < (𝐵𝑖))
227153, 154, 168, 221, 226elicod 12051 . . . . . . . . . 10 (((𝜑𝑓 ∈ ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
228145, 151, 152, 227syl21anc 1316 . . . . . . . . 9 (((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) ∧ 𝑖𝑋) → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
229228ex 448 . . . . . . . 8 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝑖𝑋 → (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
230144, 229ralrimi 2939 . . . . . . 7 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖)))
231141, 230jca 552 . . . . . 6 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → (𝑓 Fn 𝑋 ∧ ∀𝑖𝑋 (𝑓𝑖) ∈ ((𝐴𝑖)[,)(𝐵𝑖))))
232231, 86sylibr 222 . . . . 5 ((𝜑𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))) → 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)))
233232ex 448 . . . 4 (𝜑 → (𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) → 𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖))))
234109, 233impbid 200 . . 3 (𝜑 → (𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
235234alrimiv 1841 . 2 (𝜑 → ∀𝑓(𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
236 dfcleq 2603 . 2 (X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) = 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))) ↔ ∀𝑓(𝑓X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) ↔ 𝑓 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖)))))
237235, 236sylibr 222 1 (𝜑X𝑖𝑋 ((𝐴𝑖)[,)(𝐵𝑖)) = 𝑖𝑋 ((𝑖(𝐻𝑋)(𝐵𝑖)) ∖ (𝑖(𝐻𝑋)(𝐴𝑖))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  wal 1472   = wceq 1474  wex 1694  wcel 1976  wne 2779  wral 2895  Vcvv 3172  cdif 3536  wss 3539  c0 3873  ifcif 4035   ciin 4450   class class class wbr 4577  cmpt 4637   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  cmpt2 6529  Xcixp 7771  Fincfn 7818  cr 9791  -∞cmnf 9928  *cxr 9929   < clt 9930  cle 9931  (,)cioo 12002  [,)cico 12004
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-pre-lttri 9866  ax-pre-lttrn 9867
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-iin 4452  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-po 4949  df-so 4950  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7036  df-2nd 7037  df-er 7606  df-ixp 7772  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-ioo 12006  df-ico 12008
This theorem is referenced by:  hoimbllem  39317
  Copyright terms: Public domain W3C validator