# Metamath Proof Explorer

## Theorem hspdifhsp

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)

Ref Expression
Hypotheses hspdifhsp.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
hspdifhsp.n ${⊢}{\phi }\to {X}\ne \varnothing$
hspdifhsp.a ${⊢}{\phi }\to {A}:{X}⟶ℝ$
hspdifhsp.b ${⊢}{\phi }\to {B}:{X}⟶ℝ$
hspdifhsp.h ${⊢}{H}=\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)$
Assertion hspdifhsp ${⊢}{\phi }\to \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)=\bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 hspdifhsp.x ${⊢}{\phi }\to {X}\in \mathrm{Fin}$
2 hspdifhsp.n ${⊢}{\phi }\to {X}\ne \varnothing$
3 hspdifhsp.a ${⊢}{\phi }\to {A}:{X}⟶ℝ$
4 hspdifhsp.b ${⊢}{\phi }\to {B}:{X}⟶ℝ$
5 hspdifhsp.h ${⊢}{H}=\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)$
6 nfv ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{\phi }$
7 nfcv ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}{f}$
8 nfixp1 ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}\underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)$
9 7 8 nfel ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)$
10 6 9 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)$
11 ixpfn ${⊢}{f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\to {f}Fn{X}$
12 11 ad2antlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}Fn{X}$
13 fveq2 ${⊢}{k}={i}\to {B}\left({k}\right)={B}\left({i}\right)$
14 13 oveq2d ${⊢}{k}={i}\to \left(\mathrm{-\infty },{B}\left({k}\right)\right)=\left(\mathrm{-\infty },{B}\left({i}\right)\right)$
15 iftrue ${⊢}{k}={i}\to if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)=\left(\mathrm{-\infty },{B}\left({i}\right)\right)$
16 14 15 eqtr4d ${⊢}{k}={i}\to \left(\mathrm{-\infty },{B}\left({k}\right)\right)=if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
17 eqimss ${⊢}\left(\mathrm{-\infty },{B}\left({k}\right)\right)=if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\to \left(\mathrm{-\infty },{B}\left({k}\right)\right)\subseteq if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
18 16 17 syl ${⊢}{k}={i}\to \left(\mathrm{-\infty },{B}\left({k}\right)\right)\subseteq if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
19 ioossre ${⊢}\left(\mathrm{-\infty },{B}\left({k}\right)\right)\subseteq ℝ$
20 iffalse ${⊢}¬{k}={i}\to if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)=ℝ$
21 19 20 sseqtrrid ${⊢}¬{k}={i}\to \left(\mathrm{-\infty },{B}\left({k}\right)\right)\subseteq if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
22 18 21 pm2.61i ${⊢}\left(\mathrm{-\infty },{B}\left({k}\right)\right)\subseteq if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
23 mnfxr ${⊢}\mathrm{-\infty }\in {ℝ}^{*}$
24 23 a1i ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
25 4 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {B}\left({k}\right)\in ℝ$
26 25 rexrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {B}\left({k}\right)\in {ℝ}^{*}$
27 26 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {B}\left({k}\right)\in {ℝ}^{*}$
28 3 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {A}\left({k}\right)\in ℝ$
29 icossre ${⊢}\left({A}\left({k}\right)\in ℝ\wedge {B}\left({k}\right)\in {ℝ}^{*}\right)\to \left[{A}\left({k}\right),{B}\left({k}\right)\right)\subseteq ℝ$
30 28 26 29 syl2anc ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to \left[{A}\left({k}\right),{B}\left({k}\right)\right)\subseteq ℝ$
31 30 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to \left[{A}\left({k}\right),{B}\left({k}\right)\right)\subseteq ℝ$
32 simpl ${⊢}\left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\wedge {k}\in {X}\right)\to {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)$
33 simpr ${⊢}\left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\wedge {k}\in {X}\right)\to {k}\in {X}$
34 fveq2 ${⊢}{i}={k}\to {A}\left({i}\right)={A}\left({k}\right)$
35 fveq2 ${⊢}{i}={k}\to {B}\left({i}\right)={B}\left({k}\right)$
36 34 35 oveq12d ${⊢}{i}={k}\to \left[{A}\left({i}\right),{B}\left({i}\right)\right)=\left[{A}\left({k}\right),{B}\left({k}\right)\right)$
37 36 fvixp ${⊢}\left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in \left[{A}\left({k}\right),{B}\left({k}\right)\right)$
38 32 33 37 syl2anc ${⊢}\left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in \left[{A}\left({k}\right),{B}\left({k}\right)\right)$
39 38 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in \left[{A}\left({k}\right),{B}\left({k}\right)\right)$
40 31 39 sseldd ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in ℝ$
41 40 mnfltd ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to \mathrm{-\infty }<{f}\left({k}\right)$
42 28 rexrd ${⊢}\left({\phi }\wedge {k}\in {X}\right)\to {A}\left({k}\right)\in {ℝ}^{*}$
43 42 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {A}\left({k}\right)\in {ℝ}^{*}$
44 icoltub ${⊢}\left({A}\left({k}\right)\in {ℝ}^{*}\wedge {B}\left({k}\right)\in {ℝ}^{*}\wedge {f}\left({k}\right)\in \left[{A}\left({k}\right),{B}\left({k}\right)\right)\right)\to {f}\left({k}\right)<{B}\left({k}\right)$
45 43 27 39 44 syl3anc ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)<{B}\left({k}\right)$
46 24 27 40 41 45 eliood ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in \left(\mathrm{-\infty },{B}\left({k}\right)\right)$
47 22 46 sseldi ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
48 47 adantlr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
49 48 ralrimiva ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
50 12 49 jca ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to \left({f}Fn{X}\wedge \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\right)$
51 vex ${⊢}{f}\in \mathrm{V}$
52 51 elixp ${⊢}{f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)↔\left({f}Fn{X}\wedge \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\right)$
53 50 52 sylibr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
54 equequ1 ${⊢}{i}={k}\to \left({i}={l}↔{k}={l}\right)$
55 54 ifbid ${⊢}{i}={k}\to if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)=if\left({k}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)$
56 55 cbvixpv ${⊢}\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)=\underset{{k}\in {x}}{⨉}if\left({k}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)$
57 56 a1i ${⊢}\left({l}\in {x}\wedge {y}\in ℝ\right)\to \underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)=\underset{{k}\in {x}}{⨉}if\left({k}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)$
58 57 mpoeq3ia ${⊢}\left({l}\in {x},{y}\in ℝ⟼\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)=\left({l}\in {x},{y}\in ℝ⟼\underset{{k}\in {x}}{⨉}if\left({k}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)$
59 58 mpteq2i ${⊢}\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)=\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{k}\in {x}}{⨉}if\left({k}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)$
60 5 59 eqtri ${⊢}{H}=\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{k}\in {x}}{⨉}if\left({k}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)$
61 1 adantr ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {X}\in \mathrm{Fin}$
62 simpr ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {i}\in {X}$
63 4 adantr ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {B}:{X}⟶ℝ$
64 63 62 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {B}\left({i}\right)\in ℝ$
65 60 61 62 64 hspval ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {i}{H}\left({X}\right){B}\left({i}\right)=\underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
66 65 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {i}{H}\left({X}\right){B}\left({i}\right)=\underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
67 53 66 eleqtrrd ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)$
68 23 a1i ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
69 3 adantr ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {A}:{X}⟶ℝ$
70 69 62 ffvelrnd ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {A}\left({i}\right)\in ℝ$
71 70 rexrd ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {A}\left({i}\right)\in {ℝ}^{*}$
72 71 adantr ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {A}\left({i}\right)\in {ℝ}^{*}$
73 simpr ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)$
74 60 61 62 70 hspval ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {i}{H}\left({X}\right){A}\left({i}\right)=\underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
75 74 adantr ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {i}{H}\left({X}\right){A}\left({i}\right)=\underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
76 73 75 eleqtrd ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
77 62 adantr ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {i}\in {X}$
78 iftrue ${⊢}{k}={i}\to if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)=\left(\mathrm{-\infty },{A}\left({i}\right)\right)$
79 78 fvixp ${⊢}\left({f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left(\mathrm{-\infty },{A}\left({i}\right)\right)$
80 76 77 79 syl2anc ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {f}\left({i}\right)\in \left(\mathrm{-\infty },{A}\left({i}\right)\right)$
81 iooltub ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {A}\left({i}\right)\in {ℝ}^{*}\wedge {f}\left({i}\right)\in \left(\mathrm{-\infty },{A}\left({i}\right)\right)\right)\to {f}\left({i}\right)<{A}\left({i}\right)$
82 68 72 80 81 syl3anc ${⊢}\left(\left({\phi }\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {f}\left({i}\right)<{A}\left({i}\right)$
83 82 adantllr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {f}\left({i}\right)<{A}\left({i}\right)$
84 71 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {A}\left({i}\right)\in {ℝ}^{*}$
85 64 rexrd ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to {B}\left({i}\right)\in {ℝ}^{*}$
86 85 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {B}\left({i}\right)\in {ℝ}^{*}$
87 51 elixp ${⊢}{f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)↔\left({f}Fn{X}\wedge \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)$
88 87 biimpi ${⊢}{f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\to \left({f}Fn{X}\wedge \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)$
89 88 simprd ${⊢}{f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\to \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)$
90 rspa ${⊢}\left(\forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)$
91 89 90 sylan ${⊢}\left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)$
92 91 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)$
93 icogelb ${⊢}\left({A}\left({i}\right)\in {ℝ}^{*}\wedge {B}\left({i}\right)\in {ℝ}^{*}\wedge {f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\to {A}\left({i}\right)\le {f}\left({i}\right)$
94 84 86 92 93 syl3anc ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {A}\left({i}\right)\le {f}\left({i}\right)$
95 70 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {A}\left({i}\right)\in ℝ$
96 icossre ${⊢}\left({A}\left({i}\right)\in ℝ\wedge {B}\left({i}\right)\in {ℝ}^{*}\right)\to \left[{A}\left({i}\right),{B}\left({i}\right)\right)\subseteq ℝ$
97 70 85 96 syl2anc ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to \left[{A}\left({i}\right),{B}\left({i}\right)\right)\subseteq ℝ$
98 97 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to \left[{A}\left({i}\right),{B}\left({i}\right)\right)\subseteq ℝ$
99 98 92 sseldd ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℝ$
100 95 99 lenltd ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to \left({A}\left({i}\right)\le {f}\left({i}\right)↔¬{f}\left({i}\right)<{A}\left({i}\right)\right)$
101 94 100 mpbid ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to ¬{f}\left({i}\right)<{A}\left({i}\right)$
102 101 adantr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to ¬{f}\left({i}\right)<{A}\left({i}\right)$
103 83 102 pm2.65da ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to ¬{f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)$
104 67 103 eldifd ${⊢}\left(\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
105 104 ex ${⊢}\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\to \left({i}\in {X}\to {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)$
106 10 105 ralrimi ${⊢}\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\to \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
107 eliin ${⊢}{f}\in \mathrm{V}\to \left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)↔\forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)$
108 51 107 ax-mp ${⊢}{f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)↔\forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
109 106 108 sylibr ${⊢}\left({\phi }\wedge {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)\to {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
110 109 ex ${⊢}{\phi }\to \left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\to {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)$
111 n0 ${⊢}{X}\ne \varnothing ↔\exists {k}\phantom{\rule{.4em}{0ex}}{k}\in {X}$
112 111 biimpi ${⊢}{X}\ne \varnothing \to \exists {k}\phantom{\rule{.4em}{0ex}}{k}\in {X}$
113 2 112 syl ${⊢}{\phi }\to \exists {k}\phantom{\rule{.4em}{0ex}}{k}\in {X}$
114 113 adantr ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to \exists {k}\phantom{\rule{.4em}{0ex}}{k}\in {X}$
115 simpl ${⊢}\left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
116 simpr ${⊢}\left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {k}\in {X}$
117 id ${⊢}{i}={k}\to {i}={k}$
118 117 35 oveq12d ${⊢}{i}={k}\to {i}{H}\left({X}\right){B}\left({i}\right)={k}{H}\left({X}\right){B}\left({k}\right)$
119 117 34 oveq12d ${⊢}{i}={k}\to {i}{H}\left({X}\right){A}\left({i}\right)={k}{H}\left({X}\right){A}\left({k}\right)$
120 118 119 difeq12d ${⊢}{i}={k}\to \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)=\left({k}{H}\left({X}\right){B}\left({k}\right)\right)\setminus \left({k}{H}\left({X}\right){A}\left({k}\right)\right)$
121 120 eleq2d ${⊢}{i}={k}\to \left({f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)↔{f}\in \left(\left({k}{H}\left({X}\right){B}\left({k}\right)\right)\setminus \left({k}{H}\left({X}\right){A}\left({k}\right)\right)\right)\right)$
122 115 116 121 eliind ${⊢}\left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\in \left(\left({k}{H}\left({X}\right){B}\left({k}\right)\right)\setminus \left({k}{H}\left({X}\right){A}\left({k}\right)\right)\right)$
123 122 eldifad ${⊢}\left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\in \left({k}{H}\left({X}\right){B}\left({k}\right)\right)$
124 123 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\in \left({k}{H}\left({X}\right){B}\left({k}\right)\right)$
125 equequ1 ${⊢}{i}={h}\to \left({i}={l}↔{h}={l}\right)$
126 125 ifbid ${⊢}{i}={h}\to if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)=if\left({h}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)$
127 126 cbvixpv ${⊢}\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)=\underset{{h}\in {x}}{⨉}if\left({h}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)$
128 127 a1i ${⊢}\left({l}\in {x}\wedge {y}\in ℝ\right)\to \underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)=\underset{{h}\in {x}}{⨉}if\left({h}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)$
129 128 mpoeq3ia ${⊢}\left({l}\in {x},{y}\in ℝ⟼\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)=\left({l}\in {x},{y}\in ℝ⟼\underset{{h}\in {x}}{⨉}if\left({h}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)$
130 129 mpteq2i ${⊢}\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{i}\in {x}}{⨉}if\left({i}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)=\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{h}\in {x}}{⨉}if\left({h}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)$
131 5 130 eqtri ${⊢}{H}=\left({x}\in \mathrm{Fin}⟼\left({l}\in {x},{y}\in ℝ⟼\underset{{h}\in {x}}{⨉}if\left({h}={l},\left(\mathrm{-\infty },{y}\right),ℝ\right)\right)\right)$
132 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {k}\in {X}\right)\to {X}\in \mathrm{Fin}$
133 simpr ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {k}\in {X}\right)\to {k}\in {X}$
134 25 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {k}\in {X}\right)\to {B}\left({k}\right)\in ℝ$
135 131 132 133 134 hspval ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {k}\in {X}\right)\to {k}{H}\left({X}\right){B}\left({k}\right)=\underset{{h}\in {X}}{⨉}if\left({h}={k},\left(\mathrm{-\infty },{B}\left({k}\right)\right),ℝ\right)$
136 124 135 eleqtrd ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {k}\in {X}\right)\to {f}\in \underset{{h}\in {X}}{⨉}if\left({h}={k},\left(\mathrm{-\infty },{B}\left({k}\right)\right),ℝ\right)$
137 ixpfn ${⊢}{f}\in \underset{{h}\in {X}}{⨉}if\left({h}={k},\left(\mathrm{-\infty },{B}\left({k}\right)\right),ℝ\right)\to {f}Fn{X}$
138 136 137 syl ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {k}\in {X}\right)\to {f}Fn{X}$
139 138 ex ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to \left({k}\in {X}\to {f}Fn{X}\right)$
140 139 exlimdv ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to \left(\exists {k}\phantom{\rule{.4em}{0ex}}{k}\in {X}\to {f}Fn{X}\right)$
141 114 140 mpd ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to {f}Fn{X}$
142 nfii1 ${⊢}\underset{_}{Ⅎ}{i}\phantom{\rule{.4em}{0ex}}\bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
143 7 142 nfel ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}{f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
144 6 143 nfan ${⊢}Ⅎ{i}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)$
145 simpll ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {\phi }$
146 108 biimpi ${⊢}{f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
147 146 adantr ${⊢}\left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
148 simpr ${⊢}\left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {i}\in {X}$
149 rspa ${⊢}\left(\forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
150 147 148 149 syl2anc ${⊢}\left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
151 150 adantll ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$
152 simpr ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {i}\in {X}$
153 71 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {A}\left({i}\right)\in {ℝ}^{*}$
154 85 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {B}\left({i}\right)\in {ℝ}^{*}$
155 simpll ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {\phi }$
156 eldifi ${⊢}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)$
157 156 ad2antlr ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)$
158 simpr ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {i}\in {X}$
159 ioossre ${⊢}\left(\mathrm{-\infty },{B}\left({i}\right)\right)\subseteq ℝ$
160 simplr ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)$
161 65 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {i}{H}\left({X}\right){B}\left({i}\right)=\underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
162 160 161 eleqtrd ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
163 simpr ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {i}\in {X}$
164 15 fvixp ${⊢}\left({f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left(\mathrm{-\infty },{B}\left({i}\right)\right)$
165 162 163 164 syl2anc ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left(\mathrm{-\infty },{B}\left({i}\right)\right)$
166 159 165 sseldi ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℝ$
167 155 157 158 166 syl21anc ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in ℝ$
168 167 rexrd ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in {ℝ}^{*}$
169 simpl ${⊢}\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to {\phi }$
170 156 adantl ${⊢}\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)$
171 169 170 jca ${⊢}\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to \left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)$
172 171 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to \left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)$
173 simplr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {i}\in {X}$
174 simpr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}\left({i}\right)<{A}\left({i}\right)$
175 ixpfn ${⊢}{f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\to {f}Fn{X}$
176 162 175 syl ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}Fn{X}$
177 176 adantr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}Fn{X}$
178 fveq2 ${⊢}{k}={i}\to {f}\left({k}\right)={f}\left({i}\right)$
179 178 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}={i}\right)\to {f}\left({k}\right)={f}\left({i}\right)$
180 23 a1i ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
181 71 ad4ant13 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {A}\left({i}\right)\in {ℝ}^{*}$
182 166 adantr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}\left({i}\right)\in ℝ$
183 182 mnfltd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to \mathrm{-\infty }<{f}\left({i}\right)$
184 simpr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}\left({i}\right)<{A}\left({i}\right)$
185 180 181 182 183 184 eliood ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}\left({i}\right)\in \left(\mathrm{-\infty },{A}\left({i}\right)\right)$
186 185 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}={i}\right)\to {f}\left({i}\right)\in \left(\mathrm{-\infty },{A}\left({i}\right)\right)$
187 179 186 eqeltrd ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}={i}\right)\to {f}\left({k}\right)\in \left(\mathrm{-\infty },{A}\left({i}\right)\right)$
188 187 adantlr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}\in {X}\right)\wedge {k}={i}\right)\to {f}\left({k}\right)\in \left(\mathrm{-\infty },{A}\left({i}\right)\right)$
189 78 eqcomd ${⊢}{k}={i}\to \left(\mathrm{-\infty },{A}\left({i}\right)\right)=if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
190 189 adantl ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}\in {X}\right)\wedge {k}={i}\right)\to \left(\mathrm{-\infty },{A}\left({i}\right)\right)=if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
191 188 190 eleqtrd ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}\in {X}\right)\wedge {k}={i}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
192 15 159 eqsstrdi ${⊢}{k}={i}\to if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\subseteq ℝ$
193 ssid ${⊢}ℝ\subseteq ℝ$
194 20 193 eqsstrdi ${⊢}¬{k}={i}\to if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\subseteq ℝ$
195 192 194 pm2.61i ${⊢}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\subseteq ℝ$
196 162 adantr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\to {f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
197 simpr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\to {k}\in {X}$
198 fvixp2 ${⊢}\left({f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
199 196 197 198 syl2anc ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{B}\left({i}\right)\right),ℝ\right)$
200 195 199 sseldi ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in ℝ$
201 200 adantr ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\wedge ¬{k}={i}\right)\to {f}\left({k}\right)\in ℝ$
202 iffalse ${⊢}¬{k}={i}\to if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)=ℝ$
203 202 eqcomd ${⊢}¬{k}={i}\to ℝ=if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
204 203 adantl ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\wedge ¬{k}={i}\right)\to ℝ=if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
205 201 204 eleqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {k}\in {X}\right)\wedge ¬{k}={i}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
206 205 adantllr ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}\in {X}\right)\wedge ¬{k}={i}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
207 191 206 pm2.61dan ${⊢}\left(\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\wedge {k}\in {X}\right)\to {f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
208 207 ralrimiva ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
209 177 208 jca ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to \left({f}Fn{X}\wedge \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)\right)$
210 51 elixp ${⊢}{f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)↔\left({f}Fn{X}\wedge \forall {k}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({k}\right)\in if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)\right)$
211 209 210 sylibr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}\in \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)$
212 74 eqcomd ${⊢}\left({\phi }\wedge {i}\in {X}\right)\to \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)={i}{H}\left({X}\right){A}\left({i}\right)$
213 212 ad4ant13 ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to \underset{{k}\in {X}}{⨉}if\left({k}={i},\left(\mathrm{-\infty },{A}\left({i}\right)\right),ℝ\right)={i}{H}\left({X}\right){A}\left({i}\right)$
214 211 213 eleqtrd ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)$
215 172 173 174 214 syl21anc ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to {f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)$
216 eldifn ${⊢}{f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to ¬{f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)$
217 216 ad3antlr ${⊢}\left(\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\wedge {f}\left({i}\right)<{A}\left({i}\right)\right)\to ¬{f}\in \left({i}{H}\left({X}\right){A}\left({i}\right)\right)$
218 215 217 pm2.65da ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to ¬{f}\left({i}\right)<{A}\left({i}\right)$
219 155 158 70 syl2anc ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {A}\left({i}\right)\in ℝ$
220 219 167 lenltd ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to \left({A}\left({i}\right)\le {f}\left({i}\right)↔¬{f}\left({i}\right)<{A}\left({i}\right)\right)$
221 218 220 mpbird ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {A}\left({i}\right)\le {f}\left({i}\right)$
222 23 a1i ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to \mathrm{-\infty }\in {ℝ}^{*}$
223 85 adantlr ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {B}\left({i}\right)\in {ℝ}^{*}$
224 iooltub ${⊢}\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge {B}\left({i}\right)\in {ℝ}^{*}\wedge {f}\left({i}\right)\in \left(\mathrm{-\infty },{B}\left({i}\right)\right)\right)\to {f}\left({i}\right)<{B}\left({i}\right)$
225 222 223 165 224 syl3anc ${⊢}\left(\left({\phi }\wedge {f}\in \left({i}{H}\left({X}\right){B}\left({i}\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)<{B}\left({i}\right)$
226 155 157 158 225 syl21anc ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)<{B}\left({i}\right)$
227 153 154 168 221 226 elicod ${⊢}\left(\left({\phi }\wedge {f}\in \left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)$
228 145 151 152 227 syl21anc ${⊢}\left(\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\wedge {i}\in {X}\right)\to {f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)$
229 228 ex ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to \left({i}\in {X}\to {f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)$
230 144 229 ralrimi ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)$
231 141 230 jca ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to \left({f}Fn{X}\wedge \forall {i}\in {X}\phantom{\rule{.4em}{0ex}}{f}\left({i}\right)\in \left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)$
232 231 87 sylibr ${⊢}\left({\phi }\wedge {f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)\to {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)$
233 232 ex ${⊢}{\phi }\to \left({f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\to {f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)\right)$
234 110 233 impbid ${⊢}{\phi }\to \left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)↔{f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)$
235 234 alrimiv ${⊢}{\phi }\to \forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)↔{f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)$
236 dfcleq ${⊢}\underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)=\bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)↔\forall {f}\phantom{\rule{.4em}{0ex}}\left({f}\in \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)↔{f}\in \bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)\right)$
237 235 236 sylibr ${⊢}{\phi }\to \underset{{i}\in {X}}{⨉}\left[{A}\left({i}\right),{B}\left({i}\right)\right)=\bigcap _{{i}\in {X}}\left(\left({i}{H}\left({X}\right){B}\left({i}\right)\right)\setminus \left({i}{H}\left({X}\right){A}\left({i}\right)\right)\right)$